型コスモロジー：型宇宙、型銀河、ユグドラシル - 檜山正幸のキマイラ飼育記 (はてなBlog)

最近の証明支援系／プログラミング言語では、通常の型システムの上位に宇宙システム（ソートシステムともいう）を備えたものがあります。2023年の記事「最近の型理論：宇宙と世界、そして銀河」の冒頭を引用すると：

Lean（最新版はLean 4）は強力な型システムを備えた汎用プログラミング言語です。そればかりではなくて、証明支援系としての機能も同一の型システムをベースにして実現しています。AgdaやCoqもまた、型システムに基づく証明支援系／プログラミング言語です。
これら現存する最強の型システムでは、“型宇宙”がサポートされています。

特定の言語／ソフトウェアに寄らないで、一般的な宇宙システムに関する議論は「型の宇宙論」と言えます -- ここでは、「型コスモロジー」と呼ぶことにします。型コスモロジーは、型理論の一種ですが、特に宇宙に注目した型理論です。

この記事では、型コスモロジーの意味論的な側面を紹介します。つまり、型宇宙達（たくさんの型宇宙）の表示的意味論〈denotational semantics〉の枠組みをザッと述べます。型宇宙や型銀河（本文参照）の塔〈タワー〉がたくさん出てきます。グロタンディーク宇宙達／型宇宙達／型銀河達の全体の“形状”を記述する有向グラフがユグドラシルです。（北欧神話に登場するユグドラシル〈世界樹〉は、「世界を体現する巨大な木」とのことです。）

様々な宇宙達／銀河達は、何本かの塔に編成されます。主要な塔は6本です。

グロタンディーク宇宙の塔
コア銀河の塔
族銀河の塔
述語銀河の塔
データ型宇宙の塔
命題宇宙の塔

この記事では、グロタンディーク宇宙の塔とコア銀河の塔の2本の塔だけを説明します。2本の塔と、それらを“横に繋ぐ”関係性は、梯子の形をしたユグドラシル（有向グラフ）になります。

6本の塔すべてを含むユグドラシルについては、引き続く記事達で述べるつもりでいます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\twoto}{\Rightarrow}
%\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
`$

内容：

文字の色の約束
型コスモロジーの概要
グロタンディーク宇宙
グロタンディーク宇宙の存在公理と宇宙の塔
コア銀河とその塔
一般概念としての圏の塔
ユグドラシル
そしてそれから

シリーズ・ハブ記事：

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

関連記事（新しい順）：

文字の色の約束

テクニカルタームの初出または定義のとき、色を付けたテキストで書きます。よく知られた用語は青い文字です。この記事内では定義・説明しない場合もあります（調べれば分かるので）。必要なら、既存の用語の定義をここで繰り返し書くこともあります。

この記事で新しく導入・定義する用語は赤い文字です。既存の用語でも、意味を少し変えて使用する場合は赤い文字で書きます。

マゼンタの文字は、この記事内の後方で定義・説明される概念・用語です。

型コスモロジーの概要

宇宙として、集合論的宇宙と型理論的宇宙が登場します。$`\mbf{V}`$ は、ZFC集合論のフォン・ノイマン宇宙〈von Neumann universe〉です。絶対的な大宇宙として使います。フォン・ノイマン宇宙 $`\mbf{V}`$ のなかの小宇宙としてグロタンディーク宇宙〈Grothendieck universe〉がたくさん登場します。$`\mbf{V}`$ 内に存在するすべてのグロタンディーク宇宙達からなるクラスは $`\mbf{GU}`$ とします。

型宇宙〈type universe〉は、グロタンディーク宇宙をもとにして作った構造です。グロタンディーク宇宙より豊かな構造を持ちます（後でまた述べます。）。

型銀河〈type galaxy〉は、型宇宙の意味論（のモデル）となる圏のことです。三種類の型銀河を考えます。「型銀河」の前に形容詞を付けると（例：コア型銀河）、型が形容詞側にくっついて解釈され（例：コア型・銀河）そうなので、型銀河を単に「銀河」と呼びます。

コア銀河〈core galaxy〉
族銀河〈familial galaxy | galaxy of families〉
述語銀河〈predicate galaxy | galaxy of predicates〉

コア銀河は、グロタンディーク宇宙を対象達の集合〈set of objects〉とする集合圏です。単なる圏ではなくて、デカルト閉余デカルト分配圏〈Cartesian closed coCartesian distributive category〉という構造を持ちます。この圏は、足し算／掛け算／指数を持ちます。足し算／掛け算／指数という算術演算から多項式関手を定義できます。多項式関手に対する不動点／余不動点〈fixed point / cofixed point〉の存在もコア銀河の条件とします。

族銀河は、コア銀河に値を持つ族〈family〉を対象とする圏です。族は、依存型理論の主役となります。

述語銀河は、族銀河の部分圏です。コア銀河の終対象／始対象だけを値とする族が述語〈predicate〉で、対象を述語だけに絞った族銀河の部分圏が述語銀河です。述語銀河は、述語論理を（型理論的に）展開する場となります。

グロタンディーク宇宙、コア銀河、族銀河、述語銀河をパランパランに考えるのではなくて、それぞれの種類ごとに直線状の階層構造に配置します。直線状とは、順序数〈ordinal number〉に沿って並べることです。並べた系列は塔〈tower | タワー〉と呼びます。塔は単なる並びではなくて、塔としての条件（後述）があります。

次の4本の塔を考えることになります。

グロタンディーク宇宙の塔〈tower of Grothendieck universes〉
コア銀河の塔〈tower of core galaxies〉
族銀河の塔〈tower of familial galaxies〉
述語銀河の塔〈tower of predicate galaxies〉

これらの塔は、$`2\omega`$ の高さ〈height〉を持ちます（$`\omega`$ は最初の無限順序数〈infinite ordinal〉です）。

最初に触れた型宇宙は、データ型達の宇宙と命題達の宇宙に分けるのが普通です。データ型宇宙〈datatype universe〉と命題宇宙〈proposition universe〉は、グロタンディーク宇宙から直接的に作ることもできますが、それぞれ族銀河と述語銀河から構成するほうが簡単です。

データ型宇宙達と命題宇宙達も塔を形成します。

データ型宇宙の塔〈tower of datatype universes〉
命題宇宙の塔〈tower of proposition universes〉

合計6本の塔のノードとして登場する全てのグロタンディーク宇宙／コア銀河／族銀河／述語銀河／データ型宇宙／命題宇宙をインデックスするための順序集合がユグドラシル〈Yggdrasill〉です。

グロタンディーク宇宙

グロタンディーク宇宙は、フォン・ノイマン宇宙 $`\mbf{V}`$ の要素、つまり集合論の集合であって、とある条件を満たすものです。ここでは、グロタンディーク宇宙を単なる集合ではなくて構造だとみなします。グロタンディーク宇宙 $`U`$ は、その構造の構成素〈constituents〉も明示して次のように書きます。

$`\quad U = (\u{U}, \in, \{\hyp, \hyp\}, \mrm{Pow}, \cup)`$

構成素について説明します。

台集合〈underlying set〉$`\u{U}`$ ：これは、ほんとに単なる集合です。
所属関係〈membership relation〉 $`\in`$ ： $`(\in) \subseteq \u{U}\times \u{U}`$ という二項関係ですが、通常の“集合間の所属関係”です。$`\mbf{V}`$ の所属関係をそのまま使います。
順序無しペア〈unordered pair〉 $`\{\hyp, \hyp\}`$ ： $`(a, b)\mapsto \{a, b\}`$ という対応を、$`\{\hyp, \hyp\} : \u{U}\times\u{U}\to \mbf{V}`$ という関数〈写像〉と考えます。
ベキ集合〈powerset〉 $`\mrm{Pow}`$ ：ベキ集合を作る操作を、$`\u{U} \to \mbf{V}`$ という関数〈写像〉と考えます。
族の合併〈union of a family〉 $`\cup`$ ： $`\u{U}`$ から出る〈departing from $`\u{U}`$〉族（後述）達の集合を $`\msf{Fam}_{\u{U}}`$ として、族の合併を作る操作を、$`\cup : \msf{Fam}_{\u{U}} \to \mbf{V}`$ という関数〈写像〉と考えます。詳しくはすぐ下で説明します。

$`Y`$ が集合達のクラス（$`Y`$ 自身は集合でなくてもよい）として、関数 $`F: I \to Y`$ を、$`I`$-インデックス付き$`Y`$-値の族〈$`I`$-idexed $`Y`$-valued family〉と呼びます。$`X\subseteq \mbf{V}`$ をクラス（集合でなくてもよい）として、$`I\in X
`$ である族 $`F:I \to Y`$ は、$`X`$ から出る $`Y`$-値の族〈$`Y`$-valued family departing from $`X`$〉または$`X`$-発 $`Y`$-値の族と呼びます。

$`\u{U}`$-発 $`\u{U}`$-値の族の全体からなる集合が $`\msf{Fam}_{\u{U}}`$ です。$`F\in \msf{Fam}_{\u{U}}`$ とは、適当な $`I\in \u{U}`$ に対する関数 $`F: I \to \u{U}`$ のことです。

族の合併を作る関数 $`\cup`$ は、次のように定義します。

$`\text{For }I \in \u{U}`$
$`\text{For }F: I \to \u{U}`$
$`\quad \cup(F) := \bigcup_{i\in I}F(i)`$

$`U`$ がグロタンディーク宇宙である条件（グロタンディーク宇宙の公理）は以下のようです。

$`\u{U}`$ は、所属関係 $`\in`$ に関して推移的〈transitive〉である。つまり、$`x\in \u{U}, y\in x`$ ならば $`y\in \u{U}`$ となる。
関数〈演算〉$`\{\hyp, \hyp\}, \mrm{Pow}, \cup`$ に関して $`\u{U}`$ は閉じている。つまり、これらの関数は以下のように解釈してよい。
- $`\{\hyp, \hyp\} : \u{U}\times \u{U} \to \u{U}`$
- $`\mrm{Pow} : \u{U} \to \u{U}`$
- $`\cup : \msf{Fam}_{\u{U}} \to \u{U}`$

ここまで、$`U`$ と $`\u{U}`$ を区別してきましたが、以下では記号の乱用により、$`\u{U}`$ のことも $`U`$ と書きます。

すべてのグロタンディーク宇宙からなるクラスを $`\mbf{GU}`$ とします。$`\mbf{GU}`$ がどんなクラスになるかは、ZFC集合論（の公理系）からはハッキリしません。が、$`\mbf{GU}`$ が空ではないことは分かります。

まず、あまりにもつまらない例ですが、空集合 $`\emptyset`$ はグロタンディーク宇宙になります。もうひとつ、すべての遺伝的有限集合〈hereditarily finite set〉達からなる集合はグロタンディーク宇宙の構造を持ちます。遺伝的有限集合達のグロタンディーク宇宙は $`\mbf{HrdFin}`$ と書くことにします。$`\emptyset, \mbf{HrdFin} \in \mbf{GU}`$ なので、$`\mbf{GU} \ne \emptyset`$ は言えます。

グロタンディーク宇宙の存在公理と宇宙の塔

ZFC集合論（の公理系）からは、$`\mbf{GU} = \{\emptyset, \mbf{HrdFin} \}`$ なのか、それとももっと大きなクラスなのか決定できないそうです。無限集合を含むグロタンディーク宇宙が存在しないのは困るので、ZFC集合論に次の公理を加えます。

任意の集合 $`s\in \mbf{V}`$ に対して、$`s\in U`$ となるグロタンディーク宇宙 $`U`$ が存在する。

nLab項目 Grothendieck universe では、上記の公理を Axiom of Universes と呼んでいます。ここでの Universe は Grothendieck Universe なので、Axiom of Grothendieck Universes のほうが正確ですが、これだと前節で述べた「グロタンディーク宇宙が満たすべき条件である公理」と紛らわしくなってしまいます。

そういう事情で、上記の公理は単に宇宙公理と呼び、AUs と略記します。最後の s は複数形の s です -- この公理からグロタンディーク宇宙をたくさん作れるので。説明的に言いたいときは、AUs をグロタンディーク宇宙の存在公理と呼ぶことにします。

ZFC + AUs からは、$`\mbf{GU}`$ には十分に多くのグロタンディーク宇宙が含まれることが保証できます。ここでは、$`\mbf{GU}`$ 自体より、順序数の始切片〈initial segment〉から $`\mbf{GU}`$ への関数を考えます。

$`\mbf{O} \subset \mbf{V}`$ を、すべての順序数からなるクラスとします。$`\alpha \in \mbf{O}`$ として、$`\alpha`$ までの始切片は次のように定義します。

$`\quad \mbf{O}_{\lt \alpha} := \{\xi \in \mbf{O} \mid \xi \lt \alpha\}`$

特に $`\mbf{O}_{\lt\emptyset} = \emptyset`$ です。集合論の習慣に従い、$`\mbf{O}_{\lt \omega} = \mbf{N}`$ として扱います。この同一視により $`0 = \emptyset, 1 = \{\emptyset \}`$ です。

$`\mbf{O}_{\lt \alpha} \to \mbf{GU}`$ という関数も $`U, V`$ などの文字で表します。しかし、単独のグロタンディーク宇宙と紛らわしいので、引数が入る場所に $`\bullet`$ を付けて $`U_\bullet`$ のように書くことにします。例えば、$`U_\bullet : \mbf{O}_{\lt 2} \to \mbf{GU}`$ なら、2つのグロタンディーク宇宙 $`U_0, U_1`$ を表します。

順序数の始切片からの関数 $`U_\bullet : \mbf{O}_{\lt \alpha}\to \mbf{GU}`$ が次の条件を満たすとき、$`U_\bullet`$ をグロタンディーク宇宙の塔〈tower of Grothendieck universes〉と呼びます。

$`\lambda, \xi \in \mbf{O}_{\lt \alpha}`$ 、$`\lambda \lt \xi`$ ならば、$`U_\lambda \in U_\xi`$ 。

順序数 $`\alpha`$ を、塔 $`U_\bullet`$ の高さ〈height〉と呼びます。高さ $`0`$ の塔 $`\emptyset \to \mbf{GU}`$ も在りますが、これは意味がありません。高さ $`1`$ の塔 $`\{\emptyset\} \to \mbf{GU}`$ は、ひとつのグロタンディーク宇宙と同じことです。

高さが $`2\omega = \omega + \omega`$ であるグロタンディーク宇宙の塔を（超越的に）構成できます。以下のようにします。

まず、集合 $`\omega = \mbf{N}`$ を取り、宇宙公理 AUs により $`\omega \in U_0`$ となるグロタンディーク宇宙 $`U_0`$ を選びます。同様な手順で、無限の系列が作れます。

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

グロタンディーク宇宙の推移性と $`U_1 \in U_2`$ から $`U_1 \subset U_2`$ が言えます。$`U_0 \in U_1`$ と $`U_1\subset U_2`$ から $`U_0 \in U_2`$ が言えます。同様な議論を繰り返せば、次が言えます。

$`k \lt l`$ ならば、$`U_k \in U_l`$

これにより、今作った $`U_\bullet : \mbf{O}_{\lt \omega} \to \mbf{GU}`$ は塔になります。これで、高さ $`\omega`$ の塔は作れました。

次に、高さを $`\omega + 1`$ まで伸ばします。これには、新しい関数 $`{U'}_\bullet : \mbf{O}_{\lt \omega + 1} \to \mbf{GU}`$ を作る必要があります。まず、外側のフォン・ノイマン宇宙 $`\mbf{V}`$ 内で、次の集合を作ります。

$`\quad \cup(U_\bullet) = \bigcup_{k \lt \omega} U_k`$

この $`\cup(U_\bullet)`$ がグロタンディーク宇宙になるかどうかは分かりません。実際には、グロタンディーク宇宙にならないようです。しかし、宇宙公理があるので、グロタンディーク宇宙 $`{U'}_\omega`$ を次のように選べます

$`\quad \cup(U_\bullet) \in {U'}_\omega`$

この $`{U'}_\omega`$ を付け加えると、次の関数が定義できます。

$`\quad {U'}_\bullet : \mbf{O}_{\lt \omega + 1} \to \mbf{GU}`$

$`{U'}_\bullet`$ は $`\mbf{O}_{\lt \omega + 1}`$ 上の関数になっていますが、$`\mbf{O}_{\lt \omega}`$ 上では $`U_\bullet`$ とまったく同じです。

$`{U'}_\bullet`$ が塔になっているかどうかを確認します。これは、任意の自然数 $`k`$ に対して $`U_k \in {U'}_\omega`$ かどうかを確認することです。次は言えます。

$`U_k \in U_{k + 1}`$
$`U_{k + 1} \subseteq \cup(U_\bullet)`$
$`U_k \in \cup(U_\bullet)`$ （1, 2 より）
$`\cup(U_\bullet) \in {U'}_\omega`$ （定義より）

$`{U'}_\omega`$ の推移性から、$`U_k \in {U'}_\omega`$ が言えます。

さらに塔の高さを $`\omega + 2, \omega + 3, \cdots`$ と伸ばしていくのは、宇宙公理を順次適用していくだけです。

以上の手順より、$`\mbf{O}_{\lt 2\omega}`$ 上で定義されたグロタンディーク宇宙の塔が構成できます。

宇宙公理は、グロタンディーク宇宙の存在は保証しますが、その一意性は言ってません。したがって、$`\mbf{O}_{\lt 2\omega}`$ 上の塔はたくさんあるかも知れません。そのなかのひとつの塔を選んで、太字で $`\mbf{U}_\bullet`$ と書きます。太字の $`\mbf{U}_\bullet`$ は、選ばれて特定された高さ $`2\omega`$ の塔で、以下 $`\mbf{U}_\bullet`$ を固定して考えます。$`\omega \in \mbf{U}_0`$ なことに注意してください。

コア銀河とその塔

一般に、グロタンディーク宇宙 $`U`$ から作った集合圏を $`\mbf{Set}_U`$ と書きます。この定義から $`|\mbf{Set}_U| = U`$ です。より正確に言うなら $`|\mbf{Set}_U| = \u{U}`$ です。

前節で導入したグロタンディーク宇宙の塔 $`\mbf{U}_\bullet`$ に関して、次の略記を使います。

$`\quad \mbf{Set}_{\#\xi} := \mbf{Set}_{\mbf{U}_\xi}`$

順序数 $`\xi`$ が自然数のときは $`\mbf{Set}_{\#k}`$ のように書きます。$`\mbf{Set}_{\#0}`$ がデフォルトの集合圏です。

グロタンディーク宇宙の塔 $`\mbf{U}_\bullet`$ を前提として、順序数 $`\xi`$ に対する集合圏 $`\mbf{Set}_{\#\xi}`$ がコア銀河です。

フォン・ノイマン宇宙 $`\mbf{V}`$ を対象達のクラスとする集合圏を $`\mbf{SET}`$ と書くことにします。通常 $`\mbf{SET}`$ は、$`\mbf{Set}_{\#1}`$ の意味で使いますが、この記事では、究極的に大きな集合圏が $`\mbf{SET}`$ です。同様に、究極的に大きな“圏達の2-圏”は $`\mbf{CAT}`$ とします。

$`\xi \in \mbf{O}_{\lt 2\omega}`$ に $`\mbf{Set}_{\#\alpha}`$ を対応させる関数は次のように書けます。

$`\quad \mbf{Set}_{\#\bullet} : \mbf{O}_{\lt 2\omega} \to |\mbf{CAT}|`$

$`\mbf{Set}_{\#\bullet}`$ の作り方から、次が言えます。

$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`|\mbf{Set}_{\#\lambda}| \in |\mbf{Set}_{\#\xi}|`$ （所属）
$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`|\mbf{Set}_{\#\lambda}| \subset |\mbf{Set}_{\#\xi}|`$ （真部分集合）
$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`\mbf{Set}_{\#\lambda} \subset_{\mrm{full}} \mbf{Set}_{\#\xi}`$ 、ここで、$`\subset_\mrm{full}`$ は、真の部分圏でかつ充満部分圏であることを示します。

上の3つの性質を持つことも込めて、関数 $`\mbf{Set}_{\#\bullet} : \mbf{O}_{\lt 2\omega} \to |\mbf{CAT}|`$ をコア銀河の塔と呼びます。

一般概念としての圏の塔

次のような関数を考えます。

$`\quad \cat{C}_\bullet : \mbf{O}_{\lt \alpha} \to |\mbf{CAT}|`$

ここで、$`\mbf{CAT}`$ は、前節で述べたように究極的に大きな“圏達の2-圏”です。$`|\mbf{CAT}|`$ は集合ではない真のクラスですが、$`\mbf{O}_{\lt \alpha}`$ は集合なので、関数 $`\cat{C}_{\bullet}`$ を考えることはギリギリ許されるでしょう。

関数 $`\cat{C}_{\bullet}`$ が以下の条件を満たすとき、圏の塔〈tower of categories〉と呼ぶことにします（「圏の塔」は別な意味で使われることがあるので注意）。

$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`|\cat{C}_{\lambda}| \in |\cat{C}_{\xi}|`$ （所属）
$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`|\cat{C}_{\lambda}| \subseteq |\cat{C}_{\xi}|`$ （部分集合）
$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`\cat{C}_{\lambda} \subseteq_{\mrm{full}} \cat{C}_{\xi}`$ （充満部分圏）

真部分集合と真の部分圏の条件が入ってませんが、1番目の所属の条件から、真部分集合／真の部分圏であることは言えます。

圏の塔は、前節のコア銀河の塔を、任意の圏に一般化した概念です。

関数 $`X_\bullet : \mbf{O}_{\lt \alpha} \to |\mbf{SET}|`$ を考えましょう。集合 $`X_\xi`$ を、離散圏と考えれば、 $`X_\bullet : \mbf{O}_{\lt \alpha} \to |\mbf{CAT}|`$ とみなせます。上の3条件は以下のようになります。

$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`X_{\lambda} \in X_{\xi}`$ （所属）
$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`X_{\lambda} \subseteq X_{\xi}`$ （部分集合）
$`\lambda, \xi \in \mbf{O}_{\lt 2\omega}`$ 、$`\lambda \lt \xi`$ ならば、$`X_{\lambda} \subseteq_{\mrm{full}} X_{\xi}`$ （充満部分圏、部分集合と同じ）

つまり、圏の塔という概念は、グロタンディーク宇宙の塔もコア銀河の塔も包摂する一般概念です。

ところで、塔の高さが $`\omega`$ ではなくて、$`2\omega = \omega + \omega`$ なのを訝しく思った人もいるでしょう。ほとんどの場合、高さ $`\omega`$ で十分です。それどころか、マックレーン〈Saunders Mac Lane〉をはじめ何人かの人が言っているように、高さ有限の塔でもほぼ間に合います。しかし、宇宙や圏の系列の極限のようなモノを作りたいことがあります。そんなときのために、高さ $`2\omega`$ まで伸ばしておいたのです。

ユグドラシル

今までの話で、塔が2本、$`\mbf{U}_\bullet`$ と $`\mbf{Set}_{\#\bullet}`$ ができました。2本の塔を同時に考えた場合は、インデキシング集合は $`\mbf{O}_{\lt 2\omega} + \mbf{O}_{\lt 2\omega}`$ です。このインデキシング集合には自然に順序が入ります。ただし、全順序ではなくなります。

$`\mbf{O}_{\lt 2\omega} + \mbf{O}_{\lt 2\omega}`$ の要素を表すのに、$`\xi@\mathrm{gr\_univ}`$ または $`\lambda@\mathrm{core\_galax}`$ の形を使います。$`\xi@\mathrm{gr\_univ}`$ は、$`\xi`$ 番目のグロタンディーク宇宙をインデックスする要素です。$`\lambda@\mathrm{core\_galax}`$ は、$`\lambda`$ 番目のコア銀河をインデックスする要素です。

順序集合 $`\mbf{O}_{\lt 2\omega} + \mbf{O}_{\lt 2\omega}`$ を生成するハッセ図〈Hasse diagram〉を、有向グラフとして定義しましょう； $`\xi@\mrm{gr\_univ}`$ から $`(\xi + 1)@\mrm{gr\_univ}`$ への辺を考えます。また、
$`k@\mrm{gr\_univ}`$ から $`\omega@\mrm{gr\_univ}`$ への辺も考えます。$`@\mrm{core\_galax}`$ 側も同様な辺を考えます。これでハッセ図ができ上がります。

ハッセ図の辺以外に、ツインタワーの各階にスカイブリッジを渡しましょう。$`\xi`$ ごとに、$`\xi@\mrm{gr\_univ}`$ から $`\xi@\mrm{gr\_univ}`$ に辺を付け足します。逆向きの $`\xi@\mrm{gr\_univ}`$ から $`\xi@\mrm{gr\_univ}`$ へも辺を付け足します。これらのスカイブリッジ辺には、次のような値割り当て〈value assignment〉を載せます。

$`\mbf{U}_\xi \mapsto \mbf{Set}_{\#\xi}`$
$`\mbf{Set}_{\#\xi} \mapsto \mbf{U}_\xi`$

これで、全体として無限の梯子のような有向グラフとなります。各ノードにはグロタンディーク宇宙またはコア銀河が対応し、辺は宇宙／銀河の関係性を示します。これが、宇宙達／銀河達から構成される世界の形状を決めるユグドラシル〈世界樹 | Yggdrasill〉です。

そしてそれから

この記事では2本の塔だけを紹介しました。冒頭で述べたように、全部で6本の塔を建てる予定です。6本の塔達が構成する摩天楼群〈skyscrapers〉については次の機会に述べます。