[0041] -- ホモトピー型理論

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

1 $\mathord {\textnormal {\textsf {IsProp}}}(A)$
2 $\prod _{x_{1},x_{2}:A}x_{1}=x_{2}$
3 $A\to \mathord {\textnormal {\textsf {IsContr}}}(A)$

証明

1から2は定義からすぐである。

2から3を示す。 $H:\prod _{x_{1},x_{2}:A}x_{1}=x_{2}$ と $$a:A$$ を仮定する。 $$a$$ があるので、 $$A$$ が可縮であることを示すには $\prod _{x:A}a=x$ の要素を構成すればよいが、 $\lambda x.H(a,x)$ でよい。

3から1を示す。 $H:A\to \mathord {\textnormal {\textsf {IsContr}}}(A)$ と $x_{1},x_{2}:A$ を仮定する。 $x_{1}=x_{2}$ が可縮であることを示すが、 $H(x_{1}):\mathord {\textnormal {\textsf {IsContr}}}(A)$ があるので、[001L]を適用すればよい。