同値の定義([001Q])が妥当なものであることを見る。同値の概念にふさわしい性質として次を示す。
\(i\)を階数、\(A,B,C:\mathcal {U}(i)\)を型、\(f:A\to B\)と\(g:B\to C\)を型、\(c:C\)を要素とすると、\((\sum _{y:\mathord {\textnormal {\textsf {Fiber}}}(g,c)}\mathord {\textnormal {\textsf {Fiber}}}(f,y.\mathord {\textnormal {\textsf {elem}}}))\mathrel {\triangleleft \triangleright }\mathord {\textnormal {\textsf {Fiber}}}(g\circ f,c)\)の要素を構成できる。
次のようにわかる。
\(i\)を階数、\(A,B,C:\mathcal {U}(i)\)を型、\(f:A\to B\)と\(g:B\to C\)を関数とする。\(f\)と\(g\)と\(g\circ f\)のうちいずれか二つが同値ならば残りの一つも同値である。つまり、次の型の要素を構成できる。
\(f\)が同値であると仮定すると、[002L]と[001K]から\(\mathord {\textnormal {\textsf {IsEquiv}}}(g)\leftrightarrow \mathord {\textnormal {\textsf {IsEquiv}}}(g\circ f)\)が従う。
\(g\)と\(g\circ f\)が同値であると仮定する。\(b:B\)を仮定する。\(r:\mathord {\textnormal {\textsf {Fiber}}}(g,g(b))\)を\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv b,\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }\)と定義する。レトラクト
\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\to A\)は同値である。
\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。関数\(\lambda x.\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {refl}}})):A\to (\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\)と\(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(z)):(\sum _{x_{1},x_{2}:A}x_{1}=x_{2})\to A\)は同値である。
\(f\equiv \lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z)\)と\(g\equiv \lambda x.\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {pair}}}(x,\mathord {\textnormal {\textsf {refl}}}))\)と\(h\equiv \lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(z))\)と定義すると、\(f\circ g\equiv \mathord {\textnormal {\textsf {id}}}\)かつ\(h\circ g\equiv \mathord {\textnormal {\textsf {id}}}\)である。[002J]より\(f\)は同値であるから、[002E]と[0026]から\(g\)も同値であると分かる。すると、再び[002E]と[0026]から\(h\)も同値であると分かる。
\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(f,g:\prod _{x:A}B(x)\)を関数とする。型\(f\sim g:\mathcal {U}(i)\)を\(\prod _{x:A}f(x)=g(x)\)と定義する。\(f\sim g\)の要素を\(f\)と\(g\)の間のホモトピー(homotopy)と呼ぶ。
\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f,g:A\to B\)を関数、\(p:f\sim g\)をホモトピーとする。\(f\)が同値ならば\(g\)も同値である。
\(q:A\to (\sum _{y_{1},y_{2}:B}y_{1}=y_{2})\)を\(\lambda x.\mathord {\textnormal {\textsf {pair}}}(f(x),\mathord {\textnormal {\textsf {pair}}}(g(x),p(x)))\)と定義すると、\((\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z))\circ q\equiv f\)かつ\((\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\circ q\equiv g\)である。[002E]と[002J]と仮定から\(q\)が同値であると分かり、すると[002E]と[002K]から\(g\)が同値であると分かる。
\(i\)を階数、\(A,B,C,D:\mathcal {U}(i)\)を型、\(f:A\to B\)と\(g:B\to C\)と\(h:C\to D\)を関数とする。\(g\circ f\)と\(h\circ g\)が同値ならば\(f\)と\(g\)と\(h\)と\(h\circ g\circ f\)も同値である。
任意の要素\(d:D\)に対して、レトラクト
\(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)))\)と定義すればよい。