\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。\(f\)が同値ならば、関数\(g,h:B\to A\)とホモトピー\(p:f\circ g\sim \mathord {\textnormal {\textsf {id}}}\)と\(q:h\circ f\sim \mathord {\textnormal {\textsf {id}}}\)を構成できる。
証明
\(f\)が同値であると仮定する。関数\(G:\prod _{y:B}\mathord {\textnormal {\textsf {Fiber}}}(f,y)\)と同一視\(P:\prod _{y:B}\prod _{z:\mathord {\textnormal {\textsf {Fiber}}}(f,y)}G(y)=z\)を得る。\(g\equiv \lambda y.(G(y)).\mathord {\textnormal {\textsf {elem}}}\)と\(p\equiv \lambda y.(G(y)).\mathord {\textnormal {\textsf {id}}}\)と定義する。\(r:\prod _{x:A}\mathord {\textnormal {\textsf {Fiber}}}(f,f(x))\)を\(r\equiv \lambda x.\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv x,\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }\)と定義する。\(h\equiv g\)と定義し、\(q\equiv \lambda x.\mathord {\textnormal {\textsf {ap}}}(\lambda z.z.\mathord {\textnormal {\textsf {id}}},P(f(x),r(x)))\)と定義すればよい。