[0026] 補題\(i\)を階数、\(A:\mathcal {U}(i)\)を型とすると、関数\(\mathord {\textnormal {\textsf {id}}}:A\to A\)は同値である。証明\(a:A\)を要素とする。\(\mathord {\textnormal {\textsf {Fiber}}}(\mathord {\textnormal {\textsf {id}}},a)\)の定義から、\(\sum _{x:A}x=a\)が可縮であることを示せばよい。[0027]より\(x=a\)は\(a=x\)のレトラクトなので、[001S]より\(\sum _{x:A}x=a\)は可縮である。