\(i\)を階数とする。\(\mathcal {U}_{\bullet }(i)\) ([008A])の同一視型を特徴付ける。\(A:\mathcal {U}_{\bullet }(i)\)に対し、\(E:\mathcal {U}_{\bullet }(i)\to \mathcal {U}(i)\)を\(\lambda Z.(\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq Z.\mathord {\textnormal {\textsf {Carrier}}}}e(A.\mathord {\textnormal {\textsf {point}}})=Z.\mathord {\textnormal {\textsf {point}}})\)と定義する。要素\(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {id}}},\mathord {\textnormal {\textsf {refl}}}):E(A)\)を得る。レトラクトの列

\(\sum _{Z:\mathcal {U}_{\bullet }(i)}E(Z)\)\(\triangleleft \) {並び換え}\(\sum _{X:\mathcal {U}(i)}\sum _{e:A.\mathord {\textnormal {\textsf {Carrier}}}\simeq X}\sum _{x:X}e(A.\mathord {\textnormal {\textsf {point}}})=x\)\(\triangleleft \) {一価性}\(\sum _{x:A.\mathord {\textnormal {\textsf {Carrier}}}}A.\mathord {\textnormal {\textsf {point}}}=x\) を得て、最後の型は[001N]より可縮なので、\(\sum _{Z:\mathcal {U}_{\bullet }(i)}E(Z)\)は可縮である。