[003Z] 命題

$$-2$$ 型は可縮な型であり、すべての次元の構造が自明であるという最も単純な型である。次に単純な型は $$-1$$ 型である。定義から、 $$A$$ が $$-1$$ 型であるとは、任意の $x_{1},x_{2}:A$ に対して $x_{1}=x_{2}$ が可縮であることである。つまり、任意の二つの要素の間にただ一つだけ同一視がある。 $$A$$ を $$-1$$ 型とすると、 $$A$$ の要素が存在するという情報には意味があるが、 $$A$$ の二つの要素が同一かどうかは考える意味がない。このような $$A$$ を命題と考え、 $$A$$ の要素を命題の証明と考える。

[0040] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。型 $\mathord {\textnormal {\textsf {IsProp}}}(A):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {IsTrunc}}}(-1,A)$ と定義する。 $\mathord {\textnormal {\textsf {IsProp}}}(A)$ の要素がある時、 $$A$$ は命題(proposition)であると言う。

[004G] 例

$\mathbf {0}$ は命題である。実際、帰納法で直ちに示せる。

型が命題であることを示すには次が便利である。

[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]を適用すればよい。

レコード型の同一視型を決定する場面において、命題の部分は無視できることを示す([0049])。

[006B] 補題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $P,B:A\to \mathcal {U}(i)$ を型の族、 $c:\sum _{x:A}P(x)$ を要素、 $b:B(\mathord {\textnormal {\textsf {proj}}}_{1}(c))$ を要素とする。 $\prod _{x:A}\mathord {\textnormal {\textsf {IsProp}}}(P(x))$ の要素があり、 $\sum _{x:A}B(x)$ は可縮であるならば、 $\sum _{z:\sum _{x:A}P(x)}B(\mathord {\textnormal {\textsf {proj}}}_{1}(z))$ は可縮である。

証明

並び換えによりレトラクト $(\sum _{z:\sum _{x:A}P(x)}B(\mathord {\textnormal {\textsf {proj}}}_{1}(z)))\triangleleft (\sum _{z:\sum _{x:A}B(x)}P(\mathord {\textnormal {\textsf {proj}}}_{1}(z)))$ を得る。後者は[004F]と[004X]より命題であり、要素 $\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(c),b),\mathord {\textnormal {\textsf {proj}}}_{2}(c))$ を持つので、[0041]より可縮である。

[0049] 命題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $c_{1},c_{2}:\sum _{x:A}B(x)$ を要素とする。 $\prod _{x:A}\mathord {\textnormal {\textsf {IsProp}}}(B(x))$ の要素があるならば、同値 $(c_{1}=c_{2})\simeq (\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2}))$ を得る。

証明

[001S]を適用する。[006B]より、 $\sum _{x:A}\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=x$ が可縮であることを示せばよいが、これは[001N]から従う。

[0049]より、各 $$B(x)$$ が命題の時は、 $\sum _{x:A}B(x)$ の要素の同一視に関しては二番目の要素は完全に無視される。そのため、 $\sum _{x:A}B(x)$ は要素 $$a:A$$ と要素 $$b:B(a)$$ の対のなす型というよりは、要素 $$a:A$$ であって性質 $$B(a)$$ を満たすもののなす $$A$$ の部分型であると考えられる。この視点を強調するために記法を導入する。

[004A] 記法

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族とする。関数外延性の下で $\prod _{x:A}\mathord {\textnormal {\textsf {IsProp}}}(B(x))$ の要素がある時、 $\sum _{x:A}B(x)$ のことを $\lbrace x:A\mid B(x)\rbrace$ と書くことがある。さらに、要素 $c:\lbrace x:A\mid B(x)\rbrace$ に対して、 $\mathord {\textnormal {\textsf {proj}}}_{1}$ を省略して $$c$$ そのものを $$A$$ の要素とみなすことがある。

さて、これまでいくつかの型に $\mathord {\textnormal {\textsf {IsXXX}}}$ という形の命名をしてきたが、これは(関数外延性の下で)その型が命題であることを意図している。多くの概念が可縮性を軸に定義されるので、 $\mathord {\textnormal {\textsf {IsContr}}}(A)$ が命題であること([0042])が基本的である。

[0042] 命題

関数外延性を仮定する。 $$i$$ を階数、 $A:\mathcal {U}(i)$ を型とすると、型 $\mathord {\textnormal {\textsf {IsContr}}}(A)$ は命題である。

証明

[0041]より、 $\mathord {\textnormal {\textsf {IsContr}}}(A)\to \mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {IsContr}}}(A))$ を示せばよい。 $$A$$ が可縮であると仮定する。要素 $a_{0}:A$ を得る。レトラクトの列

\mathord {\textnormal {\textsf {IsContr}}}(A)

\triangleleft

{定義}

\sum _{a:A}\prod _{x:A}a=x

\triangleleft

{

\(A\)

は可縮}

\prod _{x:A}a_{0}=x

を得て、最後の型は[001L]と[0029]より可縮である。

[0043] 系

関数外延性を仮定する。 $$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とすると、 $\mathord {\textnormal {\textsf {IsTrunc}}}(n,A)$ は命題である。

証明

[0042]と[0048]から、 $$n$$ についての帰納法で示せる。

[0044] 系

関数外延性を仮定する。 $$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とすると、 $\mathord {\textnormal {\textsf {IsEquiv}}}(f)$ は命題である。

[004N]で諸々の同値の概念も命題であることを見る。

$\mathord {\textnormal {\textsf {IsTrunc}}}(n,A)$ が命題である([0043])ということは、 $\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i)$ は $\mathcal {U}(i)$ の部分型となる。一価性公理から、その同一視型を計算できる。

[0054] 命題

一価性と関数外延性を仮定する。 $$i$$ を階数、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i)$ は $\mathord {\textnormal {\textsf {succ}}}(n)$ 型である。

証明

$A,B:\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i)$ を要素とする。一価性と[0049]と[0043]より、同値 $(A=B)\simeq (A.\mathord {\textnormal {\textsf {Type}}}\simeq B.\mathord {\textnormal {\textsf {Type}}})$ を得て、後者は[0048]と[004X]と[0052]から $$n$$ 型である。

命題の相対版も考える。

[005Y] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。型 $\mathord {\textnormal {\textsf {IsEmb}}}(f):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {IsTruncMap}}}(-1,f)$ と定義する。 $\mathord {\textnormal {\textsf {IsEmb}}}(f)$ の要素がある時、 $$f$$ は埋め込み(embedding)であると言う。

[0062] 命題

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

1 $$f$$ は埋め込みである。
2任意の $x_{1}:A$ に対して、 $\sum _{x_{2}:A}f(x_{1})=f(x_{2})$ は可縮である。

証明

[005R]より、1は任意の $x_{1},x_{2}:A$ に対して $\mathord {\textnormal {\textsf {ap}}}(f):x_{1}=x_{2}\to f(x_{1})=f(x_{2})$ が同値であることと論理的に同値である。[001S]より、これは2と論理的に同値である。