同一視型の基本定理 -- ホモトピー型理論

[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]から従う。