\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(r:\mathord {\textnormal {\textsf {Retract}}}(A,B)\)を要素、\(a_{1},a_{2}:A\)を要素とすると、\(\mathord {\textnormal {\textsf {Retract}}}(a_{1}=a_{2},r.\mathord {\textnormal {\textsf {section}}}(a_{1})=r.\mathord {\textnormal {\textsf {section}}}(a_{2}))\)の要素を構成できる。
証明
\(f\equiv r.\mathord {\textnormal {\textsf {section}}}\)と\(g\equiv r.\mathord {\textnormal {\textsf {retraction}}}\)と\(p\equiv r.\mathord {\textnormal {\textsf {r-s}}}\)と定義する。\(F:a_{1}=a_{2}\to f(a_{1})=f(a_{2})\)を\(\mathord {\textnormal {\textsf {ap}}}(f)\)と定義する。\(G:f(a_{1})=f(a_{2})\to a_{1}=a_{2}\)を\(\lambda q.(p(a_{2})\circ \mathord {\textnormal {\textsf {ap}}}(g,q))\circ {(p(a_{1}))}^{-1}\)と定義する。\(\prod _{z:a_{1}=a_{2}}G(F(z))=z\)を示すには、同一視型の帰納法により\(G(F(\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace ))=\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace \)を示せばよいが、\(G(F(\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace ))\equiv p(a_{1})\circ {(p(a_{1}))}^{-1}\)なので[0047]を適用すればよい。