$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)$は可縮である。