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

• -\(\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {unit}}}:\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {mul}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\)

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

• -\(\_:\mathord {\textnormal {\textsf {IsSet}}}(G.\mathord {\textnormal {\textsf {Carrier}}})\)
• -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.(\mathord {\textnormal {\textsf {mul}}}(G.\mathord {\textnormal {\textsf {unit}}},x))=x\)
• -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(x,G.\mathord {\textnormal {\textsf {unit}}})=x\)
• -\(\_:\prod _{x_{1},x_{2},x_{3}:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(G.\mathord {\textnormal {\textsf {mul}}}(x_{1},x_{2}),x_{3})=G.\mathord {\textnormal {\textsf {mul}}}(x_{1},G.\mathord {\textnormal {\textsf {mul}}}(x_{3},x_{3}))\)
• -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(G.\mathord {\textnormal {\textsf {inv}}}(x),x)=G.\mathord {\textnormal {\textsf {unit}}}\)
• -\(\_:\prod _{x:G.\mathord {\textnormal {\textsf {Carrier}}}}G.\mathord {\textnormal {\textsf {mul}}}(x,G.\mathord {\textnormal {\textsf {inv}}}(x))=G.\mathord {\textnormal {\textsf {unit}}}\)

型\(\mathord {\textnormal {\textsf {Group}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を\(\sum _{X:\mathord {\textnormal {\textsf {GroupStr}}}(i)}\mathord {\textnormal {\textsf {GroupAxiom}}}(X)\)と定義する。\(\mathord {\textnormal {\textsf {Group}}}(i)\)の要素を(階数\(i\)の)群(group)と呼ぶ。群\(A,B:\mathord {\textnormal {\textsf {Group}}}(i)\)に対して、同一視型\(A=B\)を計算しよう。[004X]と[0048]より\(\mathord {\textnormal {\textsf {GroupAxiom}}}(X)\)は命題であることが分かるので、[0049]より同値\((A=B)\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(A)=\mathord {\textnormal {\textsf {proj}}}_{1}(B))\)を得る。[0028]と同様に、\(\mathord {\textnormal {\textsf {proj}}}_{1}(A)=\mathord {\textnormal {\textsf {proj}}}_{1}(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 {unit}}})=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {unit}}}\)
• -\(\_:\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}))\)
• -\(\_:\prod _{x}f((\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {inv}}}(x))=(\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {inv}}}(f(x))\)

この型の要素はいわゆる群同型(group isomorphism)である。\(\mathord {\textnormal {\textsf {GroupAxiom}}}(G)\)の定義で\(\mathord {\textnormal {\textsf {IsSet}}}(G.\mathord {\textnormal {\textsf {Carrier}}})\)を落とすと、\(\mathord {\textnormal {\textsf {Group}}}(i)\)の同一視の特徴付けは演算だけでなく残りの構造も保つ同値というものになってしまう。

ちなみに、群の間の乗法を保つ関数は単位元と逆元も保つことを示せるので、群同型の型は次のレコード型とも同値である。

• -\(f:(\mathord {\textnormal {\textsf {proj}}}_{1}(A)).\mathord {\textnormal {\textsf {Carrier}}}\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(B)).\mathord {\textnormal {\textsf {Carrier}}}\)
• -\(\_:\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}))\)