一連のシリーズ記事（最初の記事は「最近の型理論： 宇宙と世界、そして銀河」）を始めた目的は、最近のプログラミング言語・証明支援系 Lean、Agda、Coq などが備えている型システムの背景となっている「階層化された宇宙達を備えた型理論」を調べて紹介することです。
宇宙ベースの型理論では、「型とは宇宙の要素である」と考えます。が、これでは不十分な気がします。なので、「最近の型理論： 型理論の構文論と意味論」で「宇宙より銀河」というキャッチフレーズを提案しました。宇宙の代わりに銀河（と呼ばれる圏）をベースにすると、「型とは銀河の対象である」となります。
型の定義は銀河の定義に吸収されるので、考えるべき課題は：
- 銀河とは何か、どう定義すべきか？
- 銀河は型理論を行う舞台として適切か？
これらの課題にうまく答えられれば、たくさんの銀河達を使った型理論 -- 多銀河型理論が作れるのではないかと思っています。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\wrld}[1]{\mathscr{#1}}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\In}{\text{ in }}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\hyp}{ \text{－} }
`$
内容：
シリーズ・ハブ記事：
銀河としての資格
銀河の役割は、型の居住地〈アビタ | 棲家〉となることです。どのような性質を持った圏なら、型の棲家にふさわしいでしょうか。シリーズの最初の記事「最近の型理論： 宇宙と世界、そして銀河」では次のように定義しています。
グロタンディーク宇宙 $`U`$ に対して、$`U`$-局所小圏 $`\cat{C}`$ がデカルト閉圏であり、離散完備かつ離散余完備なとき、$`\cat{C}`$ を $`U`$ 上の銀河〈galaxy over $`U`$〉、あるいはより短く$`U`$-銀河〈$`U`$-galaxy〉と呼ぶことにします。
この銀河の条件は厳しすぎる気もします*1。うんと条件を緩めるなら、単なるデカルト閉圏でも銀河と認めるという案もあります -- 緩め過ぎかも。適切な条件をここで再考します。
銀河には内部圏をホストしてもらいたいので、ファイバー積は必要です。そのため「最近の型理論： デカルト閉圏の外部化・内部化とスノーグローブ現象」では、引き戻し付きデカルト閉圏を導入しました。有限完備デカルト閉圏〈finitely complete cartesian closed category〉と言っても同じだし、こっちのほうが一般的呼び名でした。
有限完備デカルト閉圏には良い性質があります。それはエーレスマン夫妻〈Charles and Andrée Ehresmann〉の定理で述べられます（nLab項目 internal category // In a cartesian closed category 参照）。
- $`\cat{C}`$ が有限完備デカルト閉圏ならば、内部圏の圏 $`\mrm{Cat}(\cat{C})`$ も有限完備デカルト閉圏になる。
集合圏や圏の圏では、部分集合／部分圏の概念があります。対象のあいだに、記号 '$`\subseteq`$' で表わされる関係が欲しくなるときがあります。これをサポートするには、圏が包含系〈inclusion system〉を備える必要があります（「圏の束構造と包含的圏」参照）。ジョインやミートまで必要になるかどうか分からないので、とりあえず順序構造となる包含系を要求します*2。包含順序を備えた圏をプレ包含的圏〈pre-inclusive category〉と呼ぶことにします。
新しい（変更した）銀河としての資格〈条件〉は、プレ包含的有限完備デカルト閉圏であることだとしましょう。
- 変更点 1： 離散完備性の代わりに（離散とは限らない）有限完備性を要求する。
- 変更点 2： 離散余完備性はなくてもよいとする*3。
- 変更点 3： ブレ包含的であることを要求する。
プレ包含構造が入ってもエーレスマン夫妻の定理は成立するでしょうから、銀河達は $`\mrm{Cat}(\hyp)`$ 操作に関して“閉じている”と言えます。
銀河と世界 再論
「最近の型理論： 型理論の構文論と意味論」の「宇宙より銀河と世界」より：
「階層化された宇宙達を備えた型理論」では、まず宇宙〈universe〉達があり、「型は宇宙の要素だ」と考えます。...[snip]...
集合論的な解釈は必要ではあるのですが、圏論的型理論を展開したいので、宇宙よりは銀河〈galaxy〉（と呼ばれるデカルト閉圏）に重心を移します。$`\cat{C}`$ が銀河のとき、その宇宙は対象のクラス $`|\cat{C}|`$ として定義されます。宇宙は派生的概念で、先に銀河があると考えたいのです。
多銀河型理論は銀河を扱います。しかし、この世にあるすべての銀河を同時に考えるわけではありません。当面必要そうな銀河を組織化した集まりを世界〈world〉と呼びます。
“この世にあるすべての銀河”と、ひとつの世界〈a world〉に含まれる“銀河の集まり”は同じではありません*4。“この世にあるすべての銀河”が形成する圏（むしろ2-圏）は $`{\bf Galx}`$ とします。$`{\bf Galx}`$ をちゃんと定義するのはかなり面倒ですが、今は詳細は不要です。世界 $`\wrld{W}`$ に含まれる銀河達の集合は $`\wrld{W}_\mrm{Galx}`$ とします。
$`\wrld{W}_\mrm{Galx} \subseteq |{\bf Galx}|`$ ですが、イコールだとは言ってません。世界 $`\wrld{W}`$ は単なる銀河の集合以上の構造を持ちます。「最近の型理論： 宇宙・世界・銀河 もう少し」の図の必要な部分だけを再掲すると：
$`\xymatrix@C+1.5pc{
{\bf N}
\ar[r]^{ \mrm{Sort}_{\mathscr{W}} }_{\cong}
&{\mathscr{W}_\mrm{Core}}
\ar@/^1.5pc/[r]^{{\bf Set}_{\text{－}}}
&{\mathscr{W}_\mrm{Galx}}
\ar[l]_{ \mrm{UU}_\mathscr{W} }
}`$
これは、自然数でインデックスされたグロタンディーク宇宙の系列
$`\quad \mrm{Sort}_{\mathscr{W}}(0) \in \mrm{Sort}_{\mathscr{W}}(1) \in \mrm{Sort}_{\mathscr{W}}(2) \in \cdots`$
が存在することを示します。グロタンディーク宇宙ごとに作られた集合圏
$`\quad {\bf Set}_{\# i} := {\bf Set}_{\wrld{W} \# i} := {\bf Set}_{\mrm{Sort}_{\mathscr{W}}(i)}`$
達が、コア銀河（世界の幹）を構成します。
コア銀河だけではなくて、どの銀河 $`\cat{C} \in \wrld{W}_{\mrm{Galx}}`$ も基盤宇宙〈underpinning universe〉 $`\mrm{UU}(\cat{C}) = \mrm{UU}_\wrld{W}(\cat{C})`$ を持ち、
$`\quad \cat{C} \in |\mrm{Cat}({\bf Set}_{ \mrm{UU}(\cat{C}) })|`$
が成立します。
外部化手法（「最近の型理論： デカルト閉圏の外部化・内部化とスノーグローブ現象」参照）を使いたいなら、世界に所属する銀河は、基盤銀河（基盤宇宙の集合圏）のなかで外延的であることを要請します。
銀河の階層性
「階層化された宇宙達を備えた型理論」の宇宙は、階層的に配置されます。同様な階層性を銀河のあいだにも定義しましょう。
一般に、2つの圏 $`\cat{C}, \cat{D}`$ があり、$`\cat{D}`$ が有限完備（直積やファイバー積を持つ）とき、次の関係を定義できます。
$`\quad \cat{C} \overset{\mrm{Cat}}{\in} \cat{D} :\Iff \cat{C} \in |\mrm{Cat}(\cat{D})|`$
銀河は有限完備なので（そう定義したので）、銀河はこの関係の右辺になり得ます。
関係 $`\overset{\mrm{Cat}}{\in} `$ は推移的になりませんが、次のような系列を考えることはできます。
$`\quad \cat{C} \overset{\mrm{Cat}}{\in} \cat{D} \overset{\mrm{Cat}}{\in} \cat{E}`$
関係 $`\overset{\mrm{Cat}}{\in}`$ の定義が妥当であることは、コア銀河の階層により（ある程度は）例証されます。
$`\quad {\bf Set}_{\# 0} \overset{\mrm{Cat}}{\in}{\bf Set}_{\# 1} \overset{\mrm{Cat}}{\in}{\bf Set}_{\# 2} \overset{\mrm{Cat}}{\in} \cdots`$
また、銀河 $`\cat{C} \in \wrld{W}_\mrm{Galx}`$ に対して次が成立します。
$`\quad \cat{C} \overset{\mrm{Cat}}{\in} {\bf Set}_{\mrm{UU}(\cat{C})}`$
多銀河型理論では、宇宙の代わりに銀河を使い、宇宙の階層的関係 $`\in`$ の代わりに銀河の階層的関係 $`\overset{\mrm{Cat}}{\in}`$ を使います。
循環的階層構造
銀河の階層構造が無限に続くのではなくて、循環してしまう状況を考えましょう。これは、
$`\quad \cat{C} \overset{\mrm{Cat}}{\in} \cat{C}`$
のように見える状況のことです。
「最近の型理論： デカルト閉圏の外部化・内部化とスノーグローブ現象」で述べたように、外部化手法が使える前提で、循環的階層構造は定義できます。
適当なレベル（番号 $`i`$）の集合圏 $`{\bf Set} = {\bf Set}_{\#i}`$ と対応する“圏の2-圏” $`{\bf Cat}`$ 内で考えるとします。銀河 $`\cat{C}, \cat{D}`$ に次の関係があるとします。
- $`\cat{C} \overset{\mrm{Cat}}{\in} \cat{D} \overset{\mrm{Cat}}{\in} {\bf Set}`$
- $`\ol{\cat{C}} \simeq \cat{D} \In {\bf Cat}`$ （$`\ol{(\hyp)}`$ は外部化、 $`\simeq`$ は圏同値）
$`\ol{\cat{C}}`$ と $`\cat{D}`$ が圏同値であることから、（乱暴ですが）同一視すると、
$`\quad \cat{C} \overset{\mrm{Cat}}{\in} \ol{\cat{C}}`$
とみなせます。さらに、$`\ol{\cat{C}}`$ と $`\cat{C}`$ （外部化した圏と内部圏）も同じようなものだとみなせば、
$`\quad \cat{C} \overset{\mrm{Cat}}{\in} {\cat{C}}`$
が出てきます。
もちろん、乱暴な同一視は方便であり、内部圏の外部化と圏同値による精密な定義が必要ですが、「自分が自分に含まれる」という循環的階層構造の定式化も、多銀河型理論で可能だと言えます。
