\(i\)を階数とする。\(\mathord {\textnormal {\textsf {Magma}}}(i)\) ([008B])の同一視型を特徴付ける。\(A:\mathord {\textnormal {\textsf {Magma}}}(i)\)に対し、\(E:\mathord {\textnormal {\textsf {Magma}}}(i)\to \mathcal {U}(i)\)を

\(\lambda Z.(\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq Z.\mathord {\textnormal {\textsf {Carrier}}}}\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Carrier}}}}e(A.\mathord {\textnormal {\textsf {op}}}(x_{1},x_{2}))=Z.\mathord {\textnormal {\textsf {op}}}(e(x_{1}),e(x_{2})))\) と定義する。要素\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {id}}},\lambda (x_{1},x_{2}).\mathord {\textnormal {\textsf {refl}}}):E(A)\)を得る。レトラクトの列 \(\sum _{Z:\mathord {\textnormal {\textsf {Magma}}}(i)}E(Z)\)\(\triangleleft \) {並び換え}\(\sum _{X:\mathcal {U}(i)}\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq X}\sum _{f:X\to X\to X}\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Carrier}}}}e(A.\mathord {\textnormal {\textsf {op}}}(x_{1},x_{2}))=f(e(x_{1}),e(x_{2}))\)\(\triangleleft \) {一価性}\(\sum _{f:A.\mathord {\textnormal {\textsf {Carrier}}}\to A.\mathord {\textnormal {\textsf {Carrier}}}\to A.\mathord {\textnormal {\textsf {Carrier}}}}\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Carrier}}}}A.\mathord {\textnormal {\textsf {op}}}(x_{1},x_{2})=f(x_{1},x_{2})\) を得て、最後の型は関数外延性により可縮なので、\(\sum _{Z:\mathord {\textnormal {\textsf {Magma}}}(i)}E(Z)\)は可縮である。