[004B] 集合

$$-1$$ 型の次に単純な型は $$0$$ 型である。 $$A$$ が $$0$$ 型の時は、任意の $x_{1},x_{2}:A$ に対して $x_{1}=x_{2}$ は命題である。よって、二つの要素が同一視されるかどうかには興味があるが、どう同一視されるかは考える意味がない。このような型を集合であると考える。

[004C] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。型 $\mathord {\textnormal {\textsf {IsSet}}}(A):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {IsTrunc}}}(0,A)$ と定義する。 $\mathord {\textnormal {\textsf {IsSet}}}(A)$ の要素がある時、 $$A$$ は集合(set)であると言う。

[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]による。

型が集合であることの十分条件として、同一視型が決定可能であるというのがある([004H])。ここで、型 $$P$$ が決定可能とは、 $P+(P\to \mathbf {0})$ の要素があることを言う。

[004E] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $E:A\to A\to \mathcal {U}(i)$ を型の族、 $r:\prod _{x:A}E(x,x)$ と $f:\prod _{x_{1},x_{2}:A}E(x_{1},x_{2})\to x_{1}=x_{2}$ を関数とする。 $\prod _{x_{1},x_{2}:A}\mathord {\textnormal {\textsf {IsProp}}}(E(x_{1},x_{2}))$ の要素がある時、同値 $\prod _{x_{1}(x_{2},A)}(x_{1}=x_{2})\simeq E(x_{1},x_{2})$ を構成でき、特に $$A$$ は集合である。

証明

$$r$$ から同一視型の帰納法より関数 $g:\prod _{x_{1},x_{2}:A}x_{1}=x_{2}\to E(x_{1},x_{2})$ を得る。 $E(x_{1},x_{2})$ が命題であるという仮定から、 $$f$$ と $$g$$ はレトラクト $E(x_{1},x_{2})\triangleleft (x_{1}=x_{2})$ を定める。よって、[001S]より同値 $(x_{1}=x_{2})\simeq E(x_{1},x_{2})$ を得る。

[004H] 定理(Hedberg)

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $d:\prod _{x_{1},x_{2}:A}(x_{1}=x_{2})+(x_{1}=x_{2}\to \mathbf {0})$ を関数とすると、 $$A$$ は集合である。[Hedberg--1998-0000]

証明

[004E]を適用する。 $E:A\to A\to \mathcal {U}(i)$ を次のように定義する。 $x_{1},x_{2}:A$ に対して、 $T(x_{1},x_{2}):(x_{1}=x_{2})+(x_{1}=x_{2}\to \mathbf {0})\to \mathcal {U}(i)$ を $T(x_{1},x_{2},\mathord {\textnormal {\textsf {in}}}_{1}(z))\equiv \mathbf {1}$ と $T(x_{2},x_{2},\mathord {\textnormal {\textsf {in}}}_{2}(z))\equiv \mathbf {0}$ で定義する。 $E(x_{1},x_{2})\equiv T(x_{1},x_{2},d(x_{1},x_{2}))$ と定義する。[001O]と[004F]と[004G]から、各 $E(x_{1},x_{2})$ は命題である。関数 $g:\prod _{z}T(x_{1},x_{2},z)\to x_{1}=x_{2}$ を $g(\mathord {\textnormal {\textsf {in}}}_{1}(u),w)\equiv u$ と $g(\mathord {\textnormal {\textsf {in}}}_{2}(v),w)\equiv \mathord {\textnormal {\textsf {ind}}}_{\mathbf {0}}(w,\_)$ で定義できるので、関数 $E(x_{1},x_{2})\to x_{1}=x_{2}$ を得る。最後に、任意の $$x:A$$ に対して同値 $h:\prod _{z}T(x,x,z)\simeq \mathbf {1}$ を $h(\mathord {\textnormal {\textsf {in}}}_{1}(u))\equiv \mathord {\textnormal {\textsf {id}}}$ と $h(\mathord {\textnormal {\textsf {in}}}_{2}(v))\equiv \mathord {\textnormal {\textsf {ind}}}_{\mathbf {0}}(v(\mathord {\textnormal {\textsf {refl}}}),\_)$ と定義できるので、関数 $\prod _{x:A}E(x,x)$ を得る。