[004D] -- ホモトピー型理論

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

1 $\mathord {\textnormal {\textsf {IsSet}}}(A)$
2 $\prod _{x:A}\mathord {\textnormal {\textsf {IsContr}}}(x=x)$
3 $\prod _{x:A}\prod _{z:x=x}\mathord {\textnormal {\textsf {refl}}}=z$ (Axiom Kと呼ばれる)
4 $\prod _{x_{1},x_{2}:A}\prod _{z_{1},z_{2}:x_{1}=x_{2}}z_{1}=z_{2}$ (uniqueness of identity principle (UIP)と呼ばれる)

証明

1から2を示す。 $$A$$ が集合であると仮定する。要素 $$x:A$$ に対して、 $$x=x$$ は命題である。要素 $\mathord {\textnormal {\textsf {refl}}}:x=x$ があるので、[0041]より $$x=x$$ は可縮である。

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

4において $z_{1}$ について帰納法を使うと3そのものになるので3から4が従う。

4から1は[0041]による。