型が命題であるとは、その型の任意の2点を同一視できることであった：

定義（命題）

型族 $\isProp_{\univ{U}} : \univ{U} \to \univ{U}$ を次のように定義する。

\isProp(A) \defeq \prod_{x,y: A} \Id{x}{y}

型 $A : \univ{U}$ が命題であるとは、型 $\isProp(A)$ を持つ項を選択できることである。さらに、命題の宇宙 $\hProp_{\univ{U}} : \univ{U}^+$ を、

\hProp_{\univ{U}} \defeq \sum_{A : \univ{U}} \isProp(A)

と定義する。

命題の元は高々1つしかないので、命題のことをsubsingletonとも呼ぶ。

さて、型理論における同一視型(identity type) $\Id{x}{y}$ について、以下の公理UIP (Uniqueness of Identity Proofs)は成り立つであろうか。

公理（Uniqueness of identity proofs）

任意の型 $A$ と $x,y : A$ について、 $\Id{x}{y}$ は命題である。

IntensionalなMartin-löf型理論では、この公理を証明することができない公理Kは使わないとする。。ただし、個々の型について見ると、UIPが成り立つような型は存在し、そのような型は集合と呼ばれる：

定義（集合）

型族 $\isSet_{\univ{U}} : \univ{U} \to \univ{U}$ を次のように定義する。

\isSet(A) \defeq \prod_{x,y: A} \isProp(\Id{x}{y})

型 $A : \univ{U}$ が集合であるとは、型 $\isSet(A)$ を持つ項を選択できることである。さらに、集合の宇宙 $\hSet_{\univ{U}} : \univ{U}^+$ を、

\hSet_{\univ{U}} \defeq \sum_{A : \univ{U}} \isSet(A)

と定義する。

つまり、集合の任意の2点は、高々1通りの方法で同一視される。

本稿では「命題の宇宙 $\hProp_{\univ{U}}$ が集合である」ということを示したい。しかし、この定理の証明はそこまで自明でもない。したがって、「集合であること」と論理的同値な言明を確立し、それが命題の宇宙に対して成り立つことを見る。

完全な証明

本稿では一部の証明を省略しているが、完全な証明はAgdaで書いてある。

メタ理論

前回の記事と同様、intensionalなMartin-löf型理論をメタ理論とする。

集合の特徴付け

定義（Weakly constant function）

$A$ と $B$ を任意の型とする。写像 $f : A \to B$ がweakly constantであるとは、任意の $x,y : A$ について、 $\Id{fx}{fy}$ の元を選択できることである。

この定義がweaklyと呼ばれている理由は、 $B$ が集合であるとは限らないため、 $w(x,z)$ が「 $w(x,y)$ と $w(y,z)$ の合成」と同一視できるとは限らない、つまりcoherenceが成り立つとは限らないからである。

定義（PathConstEndo）

\mathsf{ConstEndo}(A) \defeq \sum_{f : A \to A} \mathsf{WeakConst}(f)

\mathsf{PathConstEndo}(A) \defeq \prod_{x,y : A} \mathsf{ConstEndo}(\Id{x}{y})

補題（グルーポイド則：逆射）

$A : \univ{U}$ を型、 $x,y: A$ を項とする。任意の同一視 $p : \Id{x}{y}$ について、 $p^{-1}$ は左逆射(left inverse)かつ右逆射(right inverse)になる。すなわち、

\lInv : \Id{p^{-1} \bullet p}{\refl}

と

\rInv : \Id{p \bullet p^{-1}}{\refl}

を構成できる。

証明

帰納法による。

補題（集合の特徴付け）

任意の型 $A$ について、 $\isSet(A)$ と $\mathsf{PathConstEndo}(A)$ は論理的同値である。

証明

$\isSet(A) \to \mathsf{PathConstEndo}(A)$ は本稿の残りの部分で利用しないのでここでは省略する。詳細はAgdaでの証明を見ること。

$\mathsf{PathConstEndo}(A) \to \isSet(A)$ を証明する。 $\isSet(A)$ を示すには、任意の $x,y: A$ と $p,q:\Id{x}{y}$ について、型 $\Id{p}{q}$ の項を構成する必要がある。 $w_{x,y} : \Id{x}{y} \to \Id{x}{y}$ をweakly constant functionとしたとき、写像

f : \prod_{r : \Id{x}{y}} \Id{r}{(w_{x,x}(\refl))^{-1} \bullet w_{x,y}(r)}

を次のように帰納法で定義する。

\begin{align*} f(\refl) &: \Id{\refl}{(w_{x,x}(\refl))^{-1} \bullet w_{x,x}(\refl)} \\ &\defeq \lInv^{-1} \end{align*}

ここで、 $w_{x,y}$ がweakly constant functionなので、 $\Id{w_{x,y}(p)}{w_{x,y}(q)}$ となる。この同一視を $s$ と書くと、型 $\Id{p}{q}$ を持つ項

s_\ast (f(p)) \bullet (f(q))^{-1}

を構成できる。

写像の外延性と命題の外延性

$\mathsf{PathConstEndo(\hProp_{\univ{U}})}$ を示すためには、2つの公理「写像の外延性（function extensionality）」と「命題の外延性（propositional extensionality）」が必要になる。これらはどちらもunivalence公理の帰結である。

定義（happly）

$f,g : \prod_{x : A} B(x)$ について、写像

\mathsf{happly}_{f,g} : \Id{f}{g} \to \prod_{x : A} \Id{fx}{gx}

を帰納法を用いて $\mathsf{happly}_{f,f} (\refl, x) \defeq \refl$ と定義する。

公理（写像の外延性）

$\univ{U}, \univ{V}$ を宇宙とする。

\funExt_{\univ{U},\univ{V}} : \prod_{A:\univ{U}} \prod_{B:A\to\univ{V}} \prod_{f,g:\prod_{x:A}B(x)} \isEquiv(\mathsf{happly}_{f,g})

公理（命題の外延性）

$\univ{U}$ を宇宙とする。

\propExt_{\univ{U}} : \prod_{P,Q:\hProp_{\univ{U}}} \Big( (P \to Q) \to (Q \to P) \to \Id{P}{Q} \Big)

命題の外延性はunivalence公理を $\hProp$ に制限したものと捉えられる。

主定理

補題（命題であることは命題）

命題であることは命題である。具体的には、 $\univ{U}$ を宇宙とし、写像の外延性 $\funExt_{\univ{U}, \univ{U}}$ を仮定すると、任意の型 $A : \univ{U}$ について、 $\isProp(\isProp(A))$ となる。

定理（命題の宇宙は集合）

$\univ{U}$ を宇宙とする。写像の外延性 $\funExt_{\univ{U},\univ{U}}$ と命題の外延性 $\propExt_{\univ{U}}$ を仮定したとき、 $\univ{U}$ 内の命題の宇宙は集合となる。すなわち、 $\isSet(\hProp_{\univ{U}})$ となる。

証明

$\isSet(\hProp_{\univ{U}})$ と $\mathsf{PathConstEndo}(\hProp_{\univ{U}})$ は論理的同値なので、後者を示す。

$P$ と $Q$ を任意の命題とする。命題の外延性を用いると、写像

\Id{P}{Q} \stackrel{\refl \mapsto (\id,\id)}{\longrightarrow} \big((P \to Q) \times (Q \to P)\big) \stackrel{\propExt}{\longrightarrow} \Id{P}{Q}

を構成できる。 $P$ と $Q$ が命題であることと写像の外延性により、 $(P \to Q) \times (Q \to P)$ も命題である（これは読者への練習問題とする）。したがって、この写像 $\Id{P}{Q} \to \Id{P}{Q}$ はweakly constantになる。

命題の宇宙は集合

目次

完全な証明

メタ理論

集合の特徴付け

写像の外延性と命題の外延性

主定理