[0021] 一価性から関数外延性を導く

実は、一価性公理から関数外延性公理が導出される([007D])。

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とする。関数 $p:(A\to (\sum _{x:A}B(x)))\to (A\to A)$ を $\lambda f.\lambda x.\mathord {\textnormal {\textsf {proj}}}_{1}(f(x))$ とし、型 $\mathord {\textnormal {\textsf {Sect}}}(A,B):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Fiber}}}(p,\mathord {\textnormal {\textsf {id}}})$ と定義する。

[007A] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とすると、 $\prod _{x:A}B(x)$ は $\mathord {\textnormal {\textsf {Sect}}}(A,B)$ のレトラクトである。

証明

関数 $F:(\prod _{x:A}B(x))\to \mathord {\textnormal {\textsf {Sect}}}(A,B)$ を

\lambda f.\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv \lambda x.\mathord {\textnormal {\textsf {pair}}}(x,f(x)),\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }

と定義し、関数

G:\mathord {\textnormal {\textsf {Sect}}}(A,B)\to (\prod _{x:A}B(x))

を

\lambda z.\lambda x.\mathord {\textnormal {\textsf {transport}}}(\lambda g.B(g(x)),z.\mathord {\textnormal {\textsf {id}}},\mathord {\textnormal {\textsf {proj}}}_{2}(z.\mathord {\textnormal {\textsf {elem}}}(x)))

と定義すると、

G\circ F\equiv \mathord {\textnormal {\textsf {id}}}

である。

[007B] 補題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。 $\mathcal {U}(i)$ が一価性を満たし、 $$f$$ が同値ならば、任意の型 $X:\mathcal {U}(i)$ に対して関数 $\lambda g.f\circ g:(X\to A)\to (X\to B)$ は同値である。

証明

一価性より、 $$f$$ が恒等関数の場合を示せば十分であるが、 $\lambda g.\mathord {\textnormal {\textsf {id}}}\circ g\equiv \lambda g.g$ なのでこれは同値である。

[007C] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とする。 $\prod _{x:A}\mathord {\textnormal {\textsf {IsContr}}}(B(x))$ の要素があるならば、関数 $\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x:A}B(x))\to A$ は同値である。

証明

任意の $$a:A$$ に対して、レトラクト

\mathord {\textnormal {\textsf {Fiber}}}(\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z),a)

\triangleleft

{並び換え}

\sum _{x:A}\sum _{p:x=a}B(x)

\triangleleft

{[0026]}

\(B(a)\)

を得て、最後の型は仮定より可縮である。

[007D] 定理

$$i$$ を階数とする。 $\mathcal {U}(i)$ が一価性を満たすならば、 $\mathcal {U}(i)$ のすべての関数型は関数外延性を満たす。

証明

[0029]を適用する。 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とし、各 $$B(x)$$ は可縮であると仮定する。[007C]より、関数 $\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z):(\sum _{x:A}B(x))\to A$ は同値である。これと[007B]より、 $\mathord {\textnormal {\textsf {Sect}}}(A,B)$ は可縮である。したがって、[007A]と[001K]より $\prod _{x:A}B(x)$ は可縮である。