\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。次は論理的に同値である。
- 1\(f\)は全射である。
- 2\(f\)は\(-1\)連結である。
証明
\(y:B\)を要素とする。[0041]より、\({\| \mathord {\textnormal {\textsf {Fiber}}}(f,y)\| }_{-1}\)と\(\mathord {\textnormal {\textsf {IsContr}}}({\| \mathord {\textnormal {\textsf {Fiber}}}(f,y)\| }_{-1})\)は論理的に同値であるから主張が従う。