[001R] 同一視型の基本定理

同一視型はすべての型に対して一様に定義されているが、個々の型については具体的な同一視のしかたが期待される。例えば、対型の要素 $c_{1},c_{2}:A\times B$ の「自然な」同一視のしかたは $\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})$ と $\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})$ を同一視しかつ $\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})$ と $\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2})$ を同一視することである。つまり、同値 $(c_{1}=c_{2})\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2}))\times (\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))$ を構成できると期待される([002D])。同一視型の基本定理([001S])は、この手の同値を構成する手順を与える。

型 $A:\mathcal {U}(i)$ に興味があるとして、要素 $$a:A$$ に対して同一視型の族 $\lambda x.(a=x):A\to \mathcal {U}(i)$ を特徴付けることを考える。具体的に特徴付けの候補 $B:A\to \mathcal {U}(i)$ を見つけたとしよう。これが正しいものなら、 $\mathord {\textnormal {\textsf {refl}}}$ に対応する要素 $$b:B(a)$$ があるはずである。同一視型の帰納法により、 $$b$$ は関数 $b':\prod _{x:A}a=x\to B(x)$ に拡張される。 $b'(x):a=x\to B(x)$ は「標準的」な比較関数であり、これが同値であることを示したい。 $$b'(x)$$ の同値性を定義に従って示すことは難しくはないが筋が良いとも言えない。同一視型の基本定理は、すべての $$b'(x)$$ が同値であることと $\sum _{x:A}B(x)$ が可縮であることが論理的に同値であると主張する。次の点から後者の方が示しやすい性質であると思われる。

-可縮性は様々な型の構成について閉じる(例えば[001L]や[001N])。
- $\sum _{x:A}B(x)$ の可縮性は $$a$$ や $$b$$ や $$b'$$ に依らない性質である。

[001V] 補題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $e:A\simeq B$ を同値とすると、 $\mathord {\textnormal {\textsf {Retract}}}(B,A)$ の要素を構成できる。

証明

仮定 $$e$$ から $f:A\to B$ と $H:\mathord {\textnormal {\textsf {IsEquiv}}}(f)$ を得る。任意の $$y:B$$ に対して $H(y):\mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {Fiber}}}(f,y))$ を得るので、特に関数 $G:\prod _{y:B}\mathord {\textnormal {\textsf {Fiber}}}(f,y)$ を得る。[001A]の要領で $$G$$ から関数 $g:B\to A$ と同一視 $p:\prod _{y:B}f(g(y))=y$ を得る。これで要素 $\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {retraction}}}\equiv f,\mathord {\textnormal {\textsf {section}}}\equiv g,\mathord {\textnormal {\textsf {r-s}}}\equiv p\mathclose {|\negmedspace \} }:\mathord {\textnormal {\textsf {Retract}}}(B,A)$ を構成できた。

[001X] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $c_{1},c_{2}:\sum _{x:A}B(x)$ を要素とすると、

\mathord {\textnormal {\textsf {Retract}}}(\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}),c_{1}=c_{2})

の要素を構成できる。

証明

関数 $f:(\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))\to c_{1}=c_{2}$ と $g:c_{1}=c_{2}\to (\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))$ と同一視 $p:\prod _{w}g(f(w))=w$ を構成する。 $$f$$ についてはカリー化、一般化して

f':\prod _{\lbrace x:A\rbrace }\prod _{\lbrace y:B(x)\rbrace }\prod _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=y\to c_{1}=\mathord {\textnormal {\textsf {pair}}}(x,y)

を構成すればよいが、同一視型の帰納法により

f'(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}

と定義できる。

\(g\)

は一般化して

g':\prod _{\lbrace y:\sum _{x:A}B(x)\rbrace }c_{1}=y\to (\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(y)}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(y))

を帰納法で

g'(\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})

と定義する。

\(p\)

も

\(f\)

と同様にカリー化、一般化して

p':\prod _{\lbrace x\rbrace }\prod _{\lbrace y\rbrace }\prod _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x}\prod _{w:\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=y}g'(f'(z,w))=\mathord {\textnormal {\textsf {pair}}}(z,w)

を帰納法により

p'(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {refl}}}

と定義する。

[001W] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B,C:A\to \mathcal {U}(i)$ を型の族、 $r:\prod _{x:A}\mathord {\textnormal {\textsf {Retract}}}(B(x),C(x))$ を要素とすると、 $\mathord {\textnormal {\textsf {Retract}}}(\sum _{x:A}B(x),\sum _{x:A}C(x))$ の要素を構成できる。

証明

仮定 $$r$$ から関数 $f:\prod _{\lbrace x:A\rbrace }B(x)\to C(x)$ と $g:\prod _{\lbrace x:A\rbrace }C(x)\to B(x)$ と同一視 $p:\prod _{x:A}\prod _{y:B(x)}g(f(y))=y$ を得る。関数 $F:(\sum _{x:A}B(x))\to (\sum _{x:A}C(x))$ を $\lambda z.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(z),f(\mathord {\textnormal {\textsf {proj}}}_{2}(z)))$ と定義する。関数 $G:(\sum _{x:A}C(x))\to (\sum _{x:A}B(x))$ も同様に $$g$$ を使って定義される。同一視 $P:\prod _{z:\sum _{x:A}B(x)}G(F(z))=z$ を定義するために、 $z:\sum _{x:A}B(x)$ を仮定する。構成から $\mathord {\textnormal {\textsf {proj}}}_{1}(G(F(z)))\equiv \mathord {\textnormal {\textsf {proj}}}_{1}(z)$ であり、 $p(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)):\mathord {\textnormal {\textsf {proj}}}_{2}(G(F(z)))=\mathord {\textnormal {\textsf {proj}}}_{2}(z)$ を得る。[001X]を使って、 $\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {refl}}},p(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)))$ から $$G(F(z))=z$$ の要素を構成できる。

[001S] 定理(同一視型の基本定理)

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $$a:A$$ を要素、 $B:A\to \mathcal {U}(i)$ を型の族、 $$b:B(a)$$ を要素とする。次の型は論理的に同値である。

1 $\prod _{x:A}\mathord {\textnormal {\textsf {IsEquiv}}}(\lambda (p:a=x).\mathord {\textnormal {\textsf {transport}}}(B,p,b))$
2 $\prod _{x:A}(a=x)\simeq B(x)$
3 $\prod _{x:A}\mathord {\textnormal {\textsf {Retract}}}(B(x),a=x)$
4 $\mathord {\textnormal {\textsf {IsContr}}}(\sum _{x:A}B(x))$

証明

$\lambda (p:a=x).\mathord {\textnormal {\textsf {transport}}}(B,p,b)$ の型が $a=x\to B(x)$ であることから、1から2は $\simeq$ の定義から自明である。

2から3は[001V]による。

3から4を示す。3を仮定すると、[001W]から $\mathord {\textnormal {\textsf {Retract}}}(\sum _{x:A}B(x),\sum _{x:A}a=x)$ の要素を得る。すると、[001N]と[001K]より $\sum _{x:A}B(x)$ は可縮である。

最後に4から1を示す。4を仮定し、 $$x:A$$ と $$y:B(x)$$ を仮定する。 $\mathord {\textnormal {\textsf {Fiber}}}(\lambda p.\mathord {\textnormal {\textsf {transport}}}(B,p,b),y)$ が可縮であることを示す。 $\mathord {\textnormal {\textsf {Fiber}}}$ の定義より、 $\sum _{p:a=x}\mathord {\textnormal {\textsf {transport}}}(B,p,b)=y$ が可縮であることを示せばよい。[001X]と[001K]から、 $\mathord {\textnormal {\textsf {pair}}}(a,b)=\mathord {\textnormal {\textsf {pair}}}(x,y)$ が可縮であることを示せばよいが、これは仮定と[001L]から従う。

副産物として、対の同一視型の特徴付けは既に得られている。

[002B] 系

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $c_{1},c_{2}:\sum _{x:A}B(x)$ を要素とすると、同値

(c_{1}=c_{2})\simeq (\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))

を構成できる。

証明

[001S]と[001X]による。

[001S]を適用する際に便利な補題を用意する。

[0024] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $$a:A$$ を要素とする。 $$A$$ が可縮ならば $(\sum _{x:A}B(x))\mathrel {\triangleleft \triangleright }B(a)$ の要素を構成できる。

証明

$$A$$ が可縮であると仮定する。[001L]より、関数 $p:\prod _{x:A}x=a$ を得る。関数 $f:(\sum _{x:A}B(x))\to B(a)$ を $\lambda z.\mathord {\textnormal {\textsf {transport}}}(B,p(\mathord {\textnormal {\textsf {proj}}}_{1}(z)),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$ と定義し、関数 $g:B(a)\to (\sum _{x:A}B(x))$ を $\lambda y.\mathord {\textnormal {\textsf {pair}}}(a,y)$ と定義する。定義より、任意の $z:\sum _{x:A}B(x)$ に対して、 $p(\mathord {\textnormal {\textsf {proj}}}_{1}(z)):\mathord {\textnormal {\textsf {proj}}}_{1}(z)=\mathord {\textnormal {\textsf {proj}}}_{1}(g(f(z)))$ と $\mathord {\textnormal {\textsf {refl}}}:\mathord {\textnormal {\textsf {transport}}}(B,p(\mathord {\textnormal {\textsf {proj}}}_{1}(z)),\mathord {\textnormal {\textsf {proj}}}_{2}(z))=\mathord {\textnormal {\textsf {proj}}}_{2}(g(f(z)))$ を得るので、[001X]より同一視 $q:\prod _{z}g(f(z))=z$ を得る。また、[001L]より同一視 $r:p(a)=\mathord {\textnormal {\textsf {refl}}}$ も得られるので、同一視 $\lambda y.\mathord {\textnormal {\textsf {ap}}}(\lambda w.\mathord {\textnormal {\textsf {transport}}}(B,w,y),r):\prod _{y:B(a)}f(g(y))=y$ を得る。

[0025] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $C:\prod _{x:A}B(x)\to \mathcal {U}(i)$ を型の族、 $$a:A$$ と $$b:B(a)$$ を要素とする。 $\sum _{x:A}B(x)$ が可縮ならば $(\sum _{x:A}\sum _{y:B(x)}C(x,y))\mathrel {\triangleleft \triangleright }C(a,b)$ の要素を構成できる。

証明

[0024]からすぐに従う。

[002C] 例

$a_{1},a_{2}:\mathbf {1}$ を要素とする。同値 $(a_{1}=a_{2})\simeq \mathbf {1}$ を構成しよう。[001S]を適用する。 $B:\mathbf {1}\to \mathcal {U}(0)$ を $\lambda x.\mathbf {1}$ と定義する。要素 $\mathord {\star }:B(a_{1})$ を得る。[001O]と[0024]により、 $\sum _{x:\mathbf {1}}B(x)$ は $B(a_{1})$ のレトラクトである。再び[001O]により $B(a_{1})$ は可縮なので、[001K]により $\sum _{x:\mathbf {1}}B(x)$ は可縮である。

[002D] 例

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $c_{1},c_{2}:A\times B$ を要素とする。同値 $(c_{1}=c_{2})\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2}))\times (\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))$ を構成しよう。[001S]を適用する。 $E:A\times B\to \mathcal {U}(i)$ を $\lambda z.(\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(z))\times (\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{2}(z))$ と定義する。要素 $\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {refl}}},\mathord {\textnormal {\textsf {refl}}}):E(c_{1})$ を得る。レトラクトの列

\sum _{z:A\times B}E(z)

\triangleleft

{並び換え}

\sum _{x:A}\sum _{p:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x}\sum _{y:B}\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=y

\triangleleft

{[001N]と[0025]}

\sum _{y:B}\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1})=y

を得て、最後の型は[001N]により可縮なので、[001K]より

\sum _{z:A\times B}E(z)

も可縮である。