\(i\)を階数とする。型\(\mathord {\textnormal {\textsf {RingStr}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。

• -\(\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {zero}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {plus}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {neg}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {one}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {mul}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)

要素\(R:\mathord {\textnormal {\textsf {RingStr}}}(i)\)に対して、型\(\mathord {\textnormal {\textsf {RingAxiom}}}(R):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(\_:\mathord {\textnormal {\textsf {IsSet}}}(R.\mathord {\textnormal {\textsf {Carrier}}})\)
• -\(\_:\prod _{x:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {zero}}},x)=x\)
• -\(\_:\prod _{x_{1},x_{2},x_{3}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2}),x_{3})=R.\mathord {\textnormal {\textsf {plus}}}(x_{1},R.\mathord {\textnormal {\textsf {plus}}}(x_{2},x_{3}))\)
• -\(\_:\prod _{x_{1},x_{2}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2})=R.\mathord {\textnormal {\textsf {plus}}}(x_{2},x_{1})\)
• -\(\_:\prod _{x}R.\mathord {\textnormal {\textsf {plus}}}(x,R.\mathord {\textnormal {\textsf {neg}}}(x))=R.\mathord {\textnormal {\textsf {zero}}}\)
• -\(\_:\prod _{x}R.\mathord {\textnormal {\textsf {mul}}}(R.\mathord {\textnormal {\textsf {one}}},x)=x\)
• -\(\_:\prod _{x}R.\mathord {\textnormal {\textsf {mul}}}(x,R.\mathord {\textnormal {\textsf {one}}})=x\)
• -\(\_:\prod _{x_{1},x_{2},x_{3}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {mul}}}(R.\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}),x_{3})=R.\mathord {\textnormal {\textsf {mul}}}(x_{1},R.\mathord {\textnormal {\textsf {mul}}}(x_{2},x_{3}))\)
• -\(\_:\prod _{x,y_{1},y_{2}:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {mul}}}(x,R.\mathord {\textnormal {\textsf {plus}}}(y_{1},y_{2}))=R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {mul}}}(x,y_{1}),R.\mathord {\textnormal {\textsf {mul}}}(x,y_{2}))\)
• -\(\_:\prod _{x_{1},x_{2},y:R.\mathord {\textnormal {\textsf {Carrier}}}}R.\mathord {\textnormal {\textsf {mul}}}(R.\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2}),y)=R.\mathord {\textnormal {\textsf {plus}}}(R.\mathord {\textnormal {\textsf {mul}}}(x_{1},y),R.\mathord {\textnormal {\textsf {mul}}}(x_{2},y))\)

型\(\mathord {\textnormal {\textsf {Ring}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を\(\sum _{X:\mathord {\textnormal {\textsf {RingStr}}}(i)}\mathord {\textnormal {\textsf {RingAxiom}}}(X)\)と定義する。\(\mathord {\textnormal {\textsf {Ring}}}(i)\)の要素を(階数\(i\)の)環(ring)と呼ぶ。環\(A,B:\mathord {\textnormal {\textsf {Ring}}}(i)\)に対して、同一視型\(A=B\)は次のレコード型と同値であることが分かる。

• -\(f:(\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {Carrier}}}\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\_:f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {zero}}})=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {zero}}}\)
• -\(\_:\prod _{x_{1},x_{2}}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {plus}}}(x_{1},x_{2}))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {plus}}}(f(x_{1}),f(x_{2}))\)
• -\(\_:\prod _{x}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {neg}}}(x))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {neg}}}(f(x))\)
• -\(\_:f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {one}}})=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {one}}}\)
• -\(\_:\prod _{x_{1},x_{2}}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {mul}}}(f(x_{1}),f(x_{2}))\)

この型の要素はいわゆる環同型(ring isomorphism)である。