「最近の型理論： 宇宙と世界、そして銀河」(2023-04-21) 以来、型理論で使う宇宙、つまり型宇宙に興味を持っています。型宇宙は、型達をホストする場所（「ホストする」については「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」参照）です。
型宇宙は、集合論のなかで定義できるグロタンディーク宇宙でおおよそモデル化できます。が、型宇宙はグロタンディーク宇宙そのものだ、とは言いにくいです。なんか食い違いがある。この食い違いについて考えてみます。$`\newcommand{\mrm}[1]{\mathrm{#1} }
%\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1} }
\newcommand{\u}[1]{\underline{#1} }
\newcommand{\Imp}{\Rightarrow}
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
\newcommand{\code}[1]{ \ulcorner{#1}\urcorner}
%\newcommand{\Iff}{\Leftrightarrow}
`$
内容：
ZF宇宙と世界
「集合論と言えばZFC集合論」という意見が大勢〈たいせい〉かと思います。"C"は、追加の公理である選択公理〈axiom of choice〉のことなので、土台の集合論はツェルメロ／フレンケル集合論〈Zermelo-Fraenkel set theory〉です。多くの人が"C"〈選択公理〉を支持してますが、嫌う人もいます。
ZF集合論における、「外側がない」という意味での“ほんとの”宇宙を $`\mbf{ZF}`$ とします -- ZF宇宙〈ZF universe〉と呼びましょう。選択公理を入れたZF宇宙なら $`\mbf{ZF}+\mrm{C}`$ とします。選択公理を入れると、ZF宇宙の拡がりは変わりませんが、性質が変わります。
グロタンディーク宇宙 $`U`$ に対して、対応する集合圏は $`\mbf{Set}_U`$ と書きます。同様に、ZF宇宙 $`\mbf{ZF}`$ に対応する集合圏を $`\mbf{Set}_\mbf{ZF}`$ とします。そんな圏を考えていいのか？ という疑念は湧きますが、今は楽観的に認めることにします。$`\mbf{Set}_\mbf{ZF}`$ は、究極的に大きな集合圏ですから、目立つようにフォントを変えて $`\mathbb{SET}_\mbf{ZF}`$ と書くことにします。
次が成立します。
$`\quad |\mathbb{SET}_\mbf{ZF}| = \mbf{ZF}\\
\quad \forall x, y\in \mbf{ZF}.\, \mathbb{SET}_\mbf{ZF}(x, y) \in \mbf{ZF}
`$
グロタンディーク宇宙の系列 $`U_0, U_1, U_2, \cdots`$ を考えましょう。これは自然数 $`i`$ にグロタンディーク宇宙 $`U_i`$ を割り当てる関数です。次のように書けます。
$`\quad U : \mbf{N}\ni i \mapsto U_i`$
関数 $`U_\hyp`$ の余域は何でしょうか？ 普通に考えて次ですよね。
$`\quad U : \mbf{N}\to \mbf{ZF}`$
では、この関数が住んでいる集合圏は？
$`\quad U : \mbf{N}\to \mbf{ZF} \In \mathbb{SET}_\mbf{ZF}`$
ウーン、これはさすがにマズイだろう。だって、次と同じだからな。
$`\quad U : \mbf{N}\to |\mathbb{SET}_\mbf{ZF}| \In \mathbb{SET}_\mbf{ZF}`$
グロタンディーク宇宙達 $`U_i`$ をすべて収容可能なグロタンディーク宇宙 $`W`$ を準備して、次のような $`U`$ なら大丈夫そうです。
$`\quad U : \mbf{N}\to W \In \mathbb{SET}_\mbf{ZF}\\
\quad \text{where }W \in |\mathbb{SET}_\mbf{ZF}|
`$
以下、ZF宇宙内のグロタンディーク宇宙の系列を考える場合は、上記のようなグロタンディーク宇宙 $`W`$ を考えることにします。$`W`$ は世界と呼んでおきます。「世界」は過去記事で使っていた言葉です。
「最近の型理論： 宇宙と世界、そして銀河」より：
語感としては、世界より宇宙のほうが広い感じがしますが、ここでは、世界は宇宙（と後述の銀河）の集まりだとします。
型宇宙達の階層性
$`(U_i)_{i\in \mbf{U}}`$ は“宇宙”の系列とします。が、$`U_i`$ がグロタンディーク宇宙になっていることは仮定しません。なんか知らんけど「宇宙」と呼びたい集合達が $`U_i`$ です。前節と同じく、次のように書きます。
$`\quad U : \mbf{N} \to W \In \mathbb{SET}_\mbf{ZF}`$
世界 $`W`$ はほんとのグロタンディーク宇宙です。$`W`$ 内では、普通の集合論的構成が自由にできます。$`U_i`$ 内でどの程度の集合論的構成が出来るかは、とりあえずは未定・未知です。$`U_i`$ 達をベースにして型理論をやりたいという希望ないしは下心はあるので、それぞれの $`U_i`$ は型宇宙と呼ぶことにします。そう呼ぶだけです。
型宇宙の系列 $`U = (U_i)_{i\in \mbf{N}}`$ に対して、次の条件を考えます。
- $`\forall i\in \mbf{N}.\, U_i \in U_{i + 1}`$
- $`\forall i\in \mbf{N}.\, U_i \subseteq U_{i + 1}`$
一番目の条件を満たすなら、$`U`$ は所属的階層〈membership hierarchy〉を持つといいます。二番目の条件を満たすなら、$`U`$ は包含的階層〈inclusion hierarchy〉を持つといいます。
型宇宙の系列 $`U`$ が、所属的階層と包含的階層を同時に持つなら、ラッセル方式〈Russell-style〉の型宇宙系列と呼びます。階層化された集合論をやりたくてグロタンディーク宇宙の系列を考えるときは、ラッセル方式の系列を考えます。
ルオ〈Zhaohui Luo〉の分析などによると、ラッセル方式の型宇宙系列は、型理論で使う系列としてはふさわしくないようです。ということは、ラッセル方式とは違った条件の型宇宙系列を考える必要があるということです。
タルスキ方式
タルスキ方式〈Tarski-style〉の型宇宙系列は、所属的階層も包含的階層も持ちません（少なくとも持つとは仮定しない）。その代わりにリフティング演算〈リフティング関数 | lifting {operation | function}〉とデコーディング演算〈デコーディング関数 | decoding {operation | function}〉を備えています。また、各型宇宙 $`U_i`$ はそのコード〈code〉 $`\code{U_i} = u_i \in U_{i + 1}`$ を持ちます（「型・インスタンス・宇宙とタルスキ宇宙系列」参照）。
タルスキ方式の型宇宙系列をZF集合論（"C"が入ってもいい）における解釈／モデルは見たことがないんですよね（探せばあるかも知れないけど）。これ、作ってみたいな。うまくいく自信があるわけじゃないけど。
まず、型宇宙系列が無交差〈disjoint〉だということを次のように定義します。
$`\quad \forall i, j \in \mbf{N}.\, i \ne j \Imp U_i \cap U_j = \emptyset`$
与えられた型宇宙系列 $`U = (U_i)_{i\in \mbf{N}}`$ が無交差じゃないとしても、次のようにして無交差な型宇宙系列 $`U'`$ を作れます。
$`\quad {U'}_i := \{i\}\times U_i`$
無交差な型宇宙系列は、包含的階層を持たない系列の事例になります。「型宇宙系列は無交差であるべし」とは要求しませんが、無交差な型宇宙系列を念頭に話を進めます。
$`t_i : U_i \to U_{i+1}`$ は、集合（型宇宙も集合）のあいだの単射で、型理論的な演算（例えばパイ型の構成）を保存するようなものだとします。タルスキ方式では、このような（型理論的構造に対する）単射準同型写像達 $`t_i`$ を要求します。
$`\quad t_i : U_i \to U_{i+1} \In {\bf Set}_W`$
$`t_i`$ がリフティング演算です。
リフティング演算 $`t_i`$ は単射なので、$`a\in U_i`$ と $`t_i(a) \in U_{i+1}`$ を区別しない規約（単に「みなし方」の約束）を設ければ、あたかも $`U_i \subseteq U_{i + 1}`$ のように扱えます。実際に $`U_i \subseteq U_{i + 1}`$ とは主張してないので、型理論的な問題は発生しません。型理論的な問題とは、型の居住地〈habitat〉が一意に決まらないという問題です。
無交差な型宇宙系列にリフティング演算が付いたものは、具体的に構成できそうな気がします。たぶんだけど。
デコーディング演算
デコーディング演算 $`T_i`$ が謎なんだよなー。デコーディングは、$`U_i`$ の要素だけに定義されるわけではなくて、世界に備わった演算のように思えます。
$`\quad T : W \to \,{?}\, \In \mathbb{SET}_\mbf{ZF}`$
疑問符は、$`T`$ の行き先がイマイチ分からない、ってこと。
世界 $`W`$ はZF集合論のなかでは普通の集合なので、ベキ集合 $`\mrm{Pow}(W)`$ を考えてかまいません。試行錯誤の一案として、$`T`$ は次のようだと仮定します。
$`\quad T : W \to \mrm{Pow}(W) \In \mathbb{SET}_\mbf{ZF}`$
$`T`$ は次のように定義します。
$`\text{For }a\in W\\
\quad T(a) := \{x\in W \mid x\in a \}
`$
この $`T`$ をデコーディング演算とするなら、型宇宙系列の定義を少し修正する必要があります。型宇宙系列は次のような関数です。
$`\quad U : \mbf{N} \to \mrm{Pow}(W) \In \mathbb{SET}_\mbf{ZF}`$
ただし、$`U`$ を勝手に取れるわけではなくて、次の図式を可換にする $`\u{U}`$ が存在することを条件とします。
$`\quad \xymatrix{
\mbf{N} \ar[r]^U \ar@{=}[d]
& {\mrm{Pow}(W)}
\\
\mbf{N} \ar[r]_{\u{U} }
& W \ar[u]_T
}\\
\quad \text{commutative }\In \mathbb{SET}_\mbf{ZF}
`$
$`T_i`$ は、$`T`$ を $`U_i \subseteq W`$ に制限するだけです。
以上のセットアップで、以下の命題は（真偽のほどはともかく）解釈はできます。
$`\text{For }u_i \in U_{i+1}\\
\quad T(u_i) = U_i
`$
$`U_i`$ に対して $`u_i\in U_{i+1} `$ をうまく作れるかどうかはよくわかりません。デコーディング演算の定義がこれでいいのかもよくわかりません。型理論からの要求に沿えない可能性もあります。
オチもなく締まりの無い話ですが、いまのところ、ココマデですね。
