\(i\)を階数とする。\(\mathord {\textnormal {\textsf {ReflGraph}}}(i)\) ([008C])の同一視型を特徴付ける。\(A:\mathord {\textnormal {\textsf {ReflGraph}}}(i)\)と\(Z:\mathord {\textnormal {\textsf {ReflGraph}}}(i)\)に対し、\(E(Z):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(v:A.\mathord {\textnormal {\textsf {Vertex}}}\simeq Z.\mathord {\textnormal {\textsf {Vertex}}}\)
• -\(e:\prod _{\lbrace x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Vertex}}}\rbrace }A.\mathord {\textnormal {\textsf {Edge}}}(x_{1},x_{2})\simeq Z.\mathord {\textnormal {\textsf {Edge}}}(v(x_{1}),v(x_{2}))\)
• -\(r:\prod _{x:A.\mathord {\textnormal {\textsf {Vertex}}}}e(A.\mathord {\textnormal {\textsf {refl}}}(x))=Z.\mathord {\textnormal {\textsf {refl}}}(v(x))\)

要素\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}v\equiv \mathord {\textnormal {\textsf {id}}},e\equiv \lambda (x_{1},x_{2}).\mathord {\textnormal {\textsf {id}}},r\equiv \lambda x.\mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }:E(A)\)を得る。レトラクトの列 \(\sum _{Z:\mathord {\textnormal {\textsf {ReflGraph}}}(i)}E(Z)\)\(\triangleleft \) {並び換え}\(\sum _{X:\mathcal {U}(i)}\sum _{v:A.\mathord {\textnormal {\textsf {Vertex}}}\simeq X}\sum _{Y}\sum _{e}\sum _{z}\prod _{x}\_\)\(\triangleleft \) {一価性}\(\sum _{Y:A.\mathord {\textnormal {\textsf {Vertex}}}\to A.\mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)}\sum _{e:\prod _{x_{1},x_{2}:A.\mathord {\textnormal {\textsf {Vertex}}}}A.\mathord {\textnormal {\textsf {Edge}}}(x_{1},x_{2})\simeq Y(x_{1},x_{2})}\sum _{z}\prod _{x}\_\)\(\triangleleft \) {関数外延性と一価性}\(\sum _{z:\prod _{x:A.\mathord {\textnormal {\textsf {Vertex}}}}A.\mathord {\textnormal {\textsf {Edge}}}(x,x)}\prod _{x:A.\mathord {\textnormal {\textsf {Vertex}}}}A.\mathord {\textnormal {\textsf {refl}}}(x)=z(x)\) を得て、最後の型は関数外延性により可縮なので、\(\sum _{Z:\mathord {\textnormal {\textsf {ReflGraph}}}(i)}E(Z)\)は可縮である。