最近の型理論： 宇宙・世界・銀河 もう少し

前回（昨日）の記事「最近の型理論： 宇宙と世界、そして銀河」で説明した世界構造に関して、少し補足します。$`\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
`$

内容：

シリーズ・ハブ記事：

• 最近の型理論： 宇宙と世界、そして銀河

絶対的大宇宙とグロタンディーク宇宙

“絶対的大宇宙”とは、現在の集合論〈ZFC集合論〉の宇宙です。あらゆる集合はこの宇宙内に居て、宇宙の外を考えることは出来ません。絶対的大宇宙〈absolute macrocosm〉を $`\mathbb{V}`$ で表すことにすると、次が成立します。

$`\quad x`$ は集合である $`\Iff x \in \mathbb{V}`$

所属関係〈membership relation〉の記号 '$`\in`$' を使いましたが、所属関係は本来、集合と集合のあいだの関係で、上記のように使うのは不適切です。しかし、新しい記号を作るのもナンナンデ '$`\in`$' で済ませます。

絶対的大宇宙 $`\mathbb{V}`$ 内に居るモノは集合だけで、集合と呼ばれるものは必ず $`\mathbb{V}`$ 内に居ます。空集合は要素を持ちませんが、それ以外の“モノ＝集合”は要素を持ちます。つまり、次が成立します。

$`\quad \forall x\in \mathbb{V}.(\, x \ne \emptyset \Imp (\exists y\in \mathbb{V}.\, y\in x)\,)`$

絶対的大宇宙 $`\mathbb{V}`$ 内には、アトム（空集合ではないが要素を持たないモノ）は存在しません。例えば、自然数の 3 もアトムではなくて集合で、通常は次のように定義します。

$`\quad 3 := \{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\} \}`$

$`\mathbb{V}`$ は集合ではないので、集合に対する操作は一切できません。例えば、$`\{\mathbb{V}\}`$ （単元集合）や $`\mrm{Pow}(\mathbb{V})`$ （ベキ集合）は無意味で無効な表現です。これでは不便なので、$`U\in \mathbb{V}`$ であって、$`U`$ の内部だけで自己充足的に集合論が出来るような小宇宙〈microcosm〉を考えます。それがグロタンディーク宇宙〈Grothendieck universe〉です。

Wikipedia項目「グロタンディーク宇宙」に定義がありますが、グロタンディーク宇宙は、所属関係に関して推移的で、二元集合、ベキ集合、集合族の合併に関して閉じている集合です。つまり、集合 $`U`$ がグロタンディーク宇宙である条件は、次の命題達の論理ANDで表現できます。

1. $`\forall x, y\in \mathbb{V}.\, x \in U \land y\in x \Imp y\in U`$
2. $`\forall x, y\in \mathbb{V}.\, x \in U \land y\in U \Imp \{x, y\}\in U`$
3. $`\forall x\in \mathbb{V}.\, x \in U \Imp \mrm{Pow}(x) \in U`$
4. $`\forall x, f\in \mathbb{V}.\, x \in U \land f: x \to U \Imp \bigcup_{y\in x} f(y) \in U`$

$`U = \emptyset`$ と置くと、含意命題の前件（'$`\Imp`$' の左側）が偽になり、条件は成立するので、$`\emptyset`$ はグロタンディーク宇宙になります。空なグロタンディーク宇宙を嫌って、「宇宙は空ではない」という条件や、「宇宙は特定の集合を含む」という条件を付けることもあります。

グロタンディーク宇宙の存在を保証する公理には次のようなものがあります。

1. 少なくともひとつの、自然数の集合を含むグロタンディーク宇宙が存在する。
2. 任意の集合 $`x`$ に対して、$`x`$ を要素として含むグロタンディーク宇宙が存在する。
3. 任意の集合 $`x`$ に対して、$`x`$ を要素として含むグロタンディーク宇宙で最小のものが存在する。

ZFC集合論の立場からの、これらの公理の正確な定式化や、取り扱いの方針などは、僕はよく分かりません。が、ユーザーとしては、次のようなグロタンディーク宇宙の無限系列が欲しいし、それがあれば十分な気がします。

$`\quad U_0 \in U_1 \in U_2 \in \cdots`$

関連する記事：

• グロタンディーク宇宙って何なんだ？
• あなたはこの公理を信じますか

型宇宙

型理論のための宇宙に関しては、前回記事「最近の型理論： 宇宙と世界、そして銀河」の最後に挙げた2つの論文に解説があります。

• Title: On Universes in Type Theory
• Author: Erik Palmgren
• Pages: 14p
• URL: http://www2.math.uu.se/~palmgren/universe.pdf

• Title: Notes on Universes in Type Theory
• Author: Zhaohui Luo
• Pages: 8p
• URL: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf

型理論のための宇宙は、（必要ならば、）グロタンディーク宇宙（主に圏論のための宇宙）と区別して型宇宙〈type universe〉と呼ぶことにします。

型宇宙は、マルティンレーフ〈Per Erik Rutger Martin-Löf〉が最初に定義したようです。タルスキー・スタイルの型宇宙とラッセル・スタイルの型宇宙の二種類があるとのこと。

• タルスキー・スタイルの宇宙： 宇宙 $`U`$ の要素（型コード）に対して、型へとデコードする関数 $`T`$ と、上位の宇宙 $`U'`$ に埋め込む関数 $`t`$ が存在する。
• ラッセル・スタイルの宇宙： 宇宙 $`U`$ の要素は型そのもので、$`U \subset U'`$ （累積的）である。デコード関数と埋め込み関数は不要である。

グロタンディーク宇宙（の系列）は、型宇宙とみなせばラッセル・スタイルです。タルスキー・スタイルはちょっと煩雑になります。しかし、型理論との相性はタルスキー・スタイルのほうがいいみたいです。タルスキー・スタイルにおけるデコード関数と埋め込み関数をコアージョン〈coercion | 強制〉とみなせば、明示的なデコード／埋め込み指定が不要となり、使い勝手はラッセル・スタイルと同等に出来るとルオ〈Zhaohui Luo〉が書いています。

圏論的銀河

「銀河」という言葉は過去に使ったことがありました。

• 現場の集合論としての有界素朴集合論

上記過去記事の「銀河」は、素朴集合論の文脈における概念で、話題にしている集合達をすべて含む集合です。グロタンディーク宇宙と似てますが、気持ちの上では絶対的大宇宙のように扱うので、銀河の外に出ることは考えてません。

過去記事の銀河は素朴集合論的銀河です。前回記事「最近の型理論： 宇宙と世界、そして銀河」の銀河は圏論的銀河〈categorical galaxy〉と言えるでしょう。圏論的銀河は圏の種別であり、世界の構成素です。

圏論的銀河（以下単に「銀河」）は、グロタンディーク宇宙 $`U`$ に対して相対的に定義されます。銀河は、$`U`$-局所小圏であり、$`U`$ に関して離散完備かつ離散余完備なデカルト閉圏でした。グロタンディーク宇宙 $`U`$ 上のすべての銀河からなるクラス（圏ではない）を $`\mrm{Galx}(U)`$ とします。$`\cat{C} \in \mrm{Galx}(U)`$ はハッキリとした意味を持ちます。

グロタンディーク宇宙の集合 $`\Xi`$ があったとき、
$`\quad \bigcup_{U\in \Xi} \mrm{Galx}(U)`$
と、
$`\quad \cat{C} \in \bigcup_{U\in \Xi} \mrm{Galx}(U)`$
も意味を持ちます。

世界 $`\mathscr{W}`$ に含まれる銀河の集合 $`\mathscr{W}_\mrm{Galx}`$ に関して次が成立します。

$`\quad \mathscr{W}_\mrm{Galx} \subseteq \bigcup_{U\in \mathscr{W}_\mrm{Core}} \mrm{Galx}(U)`$

世界の構造と法則

世界〈world〉 $`\mathscr{W}`$ は次の構成素を持ちます。

• コア宇宙（グロタンディーク宇宙になっている）の集合 $`\mathscr{W}_\mrm{Core}`$
• 銀河の集合 $`\mathscr{W}_\mrm{Galx}`$
• （コアとは限らない）宇宙の集合 $`\mathscr{W}_\mrm{Univ}`$
• コア宇宙の番号付けをする関数 $`\mrm{Sort}_\mathscr{W}:{\bf N} \to \mathscr{W}_\mrm{Core}`$
• 銀河に、その基盤宇宙〈underpinning universe〉を対応させる関数 $`\mrm{UU}_\mathscr{W}: \mathscr{W}_\mrm{Galx} \to \mathscr{W}_\mrm{Core}`$

構成素達をひとつの図式にまとめると：

$`\xymatrix@C+1.5pc{
{\bf N}
\ar[r]^{ \mrm{Sort}_{\mathscr{W}} }_{\cong}
&{\mathscr{W}_\mrm{Core}}
\ar@/^1.5pc/[r]^{{\bf Set}_{\text{－}}}
\ar@{^{(}->} [d]
&{\mathscr{W}_\mrm{Galx}}
\ar[dl]^{\mrm{Obj}}
\ar[l]_{ \mrm{UU}_\mathscr{W} }
\\
{}
&{\mathscr{W}_{\mrm{Univ}} }
&{}
}`$

この図式は、絶対的宇宙から作った集合圏内で解釈します。

$`\mrm{Sort}_\mathscr{W}`$ と $`\mrm{UU}_\mathscr{W}`$ は世界 $`\mathscr{W}`$ に固有の写像です。$`{\bf Set}_{\text{－}}`$ はグロタンディーク宇宙に、その集合圏を対応させる写像、$`\mrm{Obj}`$ は圏の対象クラスを取る写像です。

$`\mathscr{W}`$ が世界であるためには、次の条件〈法則 | 公理〉を満たす必要があります。

1. $`\mrm{Sort}_\mathscr{W}`$ は同型写像（1：1対応）である。
2. $`\mrm{Sort}(0) \in \mrm{Sort}(1) \in \cdots`$ はグロタンディーク宇宙の系列になる。
3. $`\mathscr{W}_\mrm{Core} \subseteq \mathscr{W}_\mrm{Univ}`$
4. $`\mathscr{W}_\mrm{Galx}`$ に制限した $`\mrm{Obj}`$ は全射。
5. $`{\bf Set}_{\text{－}}; \mrm{Obj} = \mrm{incl}`$ （右辺は包含写像）
6. $`{\bf Set}_{\text{－}} ; \mrm{UU}_\mathscr{W} = \mrm{id}_{\mathscr{W}_\mrm{Core}}`$
7. $`\mathscr{W}_\mrm{Galx} \subseteq \bigcup_{U\in \mathscr{W}_\mrm{Core}} \mrm{Galx}(U)`$

世界 $`\mathscr{W}`$ は、集合論的構造（グロタンディーク宇宙）と圏論的構造（圏論的銀河）を取り込んだ構造であり、型理論の構成と解釈に使えると期待できます。