[0009] 宇宙

型理論における対象は型と要素の二種類に分けられるが、型と要素を厳格に区別し続けることは時に理論を煩雑にする。そこで宇宙を導入する。宇宙とは要素が型であるような型である。すべての型がある宇宙の要素になるように規則を設計することで、型を特別な要素とみなすことができる。本書で考える型理論は「可算個」の非有界な宇宙の列

\mathcal {U}(0):\mathcal {U}(1):\mathcal {U}(2):\dots

を持つ。

数学を基礎付ける文脈では $0,1,2,\dots$ が何なのか分からないので、階数の概念を導入する。階数は型でも要素でもない別の種類の対象である。

[000D] 規則

階数(level)についての規則は次で与えられる。

-階数 $$0$$ を構成できる。
-階数 $$i$$ に対し、階数 $\mathord {\textnormal {\textsf {succ}}}(i)$ を構成できる。

宇宙に関する規則は次の通りである。

[000E] 規則

宇宙(universe)についての規則は次で与えられる。

-階数 $$i$$ に対して、型 $\mathcal {U}(i)$ を構成できる。
-階数 $$i$$ と要素 $A:\mathcal {U}(i)$ に対して、型 $\mathord {\textnormal {\textsf {El}}}(A)$ を構成できる。
-階数 $$i$$ に対して、要素 $\lceil \mathcal {U}\rceil (i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を構成できる。
-階数 $$i$$ に対して、 $\mathord {\textnormal {\textsf {El}}}(\lceil \mathcal {U}\rceil (i))\equiv \mathcal {U}(i)$ と定義される。
-階数 $$i$$ と要素 $A:\mathcal {U}(i)$ に対して、 $\mathord {\textnormal {\textsf {Lift}}}(A):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を構成できる。
-階数 $$i$$ と要素 $A:\mathcal {U}(i)$ に対して、 $\mathord {\textnormal {\textsf {El}}}(\mathord {\textnormal {\textsf {Lift}}}(A))\equiv \mathord {\textnormal {\textsf {El}}}(A)$ と定義される。

[000F] 記法

- $\mathord {\textnormal {\textsf {El}}}$ はよく省略する。つまり、要素 $A:\mathcal {U}(i)$ そのものを型とみなす。
- $\mathord {\textnormal {\textsf {Lift}}}$ はよく省略する。つまり、要素 $A:\mathcal {U}(i)$ は $\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ の要素でもあるとみなす。
- $\mathcal {U}(i)$ と $\lceil \mathcal {U}\rceil (i)$ を表記上区別しない。つまり、 $\mathcal {U}(i)$ そのものを $\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ の要素とみなす。

[000F]の下で、[000E]は次のようにも書ける。

-階数 $$i$$ に対して、 $\mathcal {U}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を構成できる。
-階数 $$i$$ と要素 $A:\mathcal {U}(i)$ に対して、 $$A$$ は型である。
-階数 $$i$$ と要素 $A:\mathcal {U}(i)$ に対して、 $A:\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ である。

本書で考える型理論では[000E]の他には形式的な意味での型を構成する規則は与えず、代わりに $\mathcal {U}(i)$ の要素を構成する規則を与える。以降、 $\mathcal {U}(i)$ の要素を(階数 $$i$$ の)型と呼ぶ。