前回の記事「最近の型理論： 外部化手法のもとでのパイ型と指数型」で、次のようなことを書きました。
対象を圏の外部に取り出す方法を外部化手法〈externalization〉と呼ぶとして、...[snip]...
「集合圏と似てないデカルト閉圏に対しては、外部化手法は有効じゃない」気がします。
「外部化しないでどうやるんだ？」と聞かれると、よく分かりません。
明らかなメリットがあるので、外部化手法は使い続けるかも知れませんが、完全に満足すべき状況でないのは確かです。外部化手法を改善するか、別の手法に乗り換えることを考える必要があります。
デカルト閉圏 C の対象を外部化する代わりに、$`\mathcal{C}`$ を $`\mathcal{C}`$ 自身のなかに内部化して型ファミリーを定義する方法もあるでしょう。
これらについて、その後考えたことを記します。細部にはあまり踏み込まず、全体的なアイディアと方針を述べます。半分“オハナシ”です。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\J}{\mathrm{J}}
\newcommand{\K}{\mathrm{K}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}}
`$
内容：
シリーズ・ハブ記事：
世界の構造（復習）
一連のシリーズ記事の主題は「階層化された宇宙達を備えた型理論」です。シリーズの最初の記事「最近の型理論： 宇宙と世界、そして銀河」で述べたように、階層化された宇宙達は、各宇宙から構成される“標準的集合圏”達と、付随する銀河（と呼ばれる圏）達により“世界”を形成します。どのような世界を措定するかにより、そこで展開される型理論の様相も変わってきます。
世界の幹となるのは、一列に並べられた宇宙〈グロタンディーク宇宙〉の系列です。
$`\quad U_0 \in U_1 \in U_2 \in \cdots`$
この系列を仮定するのは、異常に超越的です*1が、まーいいんじゃないかと思います -- 認めましょう。宇宙 $`U = U_i`$ ごとに集合圏 $`{\bf Set}_U`$ が付属しています。1：1に対応した宇宙と集合圏の集まりが世界のコア（コア宇宙とコア銀河）となります。
コア宇宙（一列に並んだグロタンディーク宇宙）とコア銀河（集合圏）以外の宇宙／銀河の存在も認めます。（コアまたはそれ以外の）銀河は、世界内の事物〈thing〉を収める器となる圏です。銀河はデカルト圏であることを要求します。多くの銀河はデカルト閉圏で、さらに追加の（主に極限・余極限で定義される）構造*2を持つこともあります。
我々は、デフォルトの集合圏 $`{\bf Set} = {\bf Set}_U`$ 内の$`U`$-局所小デカルト閉圏〈銀河〉 $`\cat{C}`$ を選んで、これをベース圏と呼びます。もうひとつのデカルト閉圏〈銀河〉 $`\cat{D}`$ を選んで（$`\cat{C} = \cat{D}`$ でもよい）、次のようなインデックス付き圏 $`\cat{P}`$ を作ります。
$`\quad \cat{P}[\hyp] := {\bf CAT}(\J(\hyp), \cat{C})\;\in |{\bf CAT}|`$
$`\cat{P}`$ は $`\cat{C}, \cat{D}`$ から決まるので、必要があれば次のように書きます。
$`\quad \cat{P} = \cat{P}_\cat{C}^\cat{D}`$
$`\cat{P}`$ を定義するために出てきた $`\J`$ は型圏化〈type categorification〉関手で、次のプロファイル（域〈ソース〉と余域〈ターゲット〉）を持ちます。
$`\quad \J : \cat{C} \to \dimU{\bf CAT}{1} \In \mathbb{CAT}`$
詳細は次の記事を見てください。
型圏化関手 $`\J`$ と、それのもとになる外延化関手 $`\mrm{Inst} = \ol{(\hyp)}\;`$ を使う手法が外部化〈externalization〉手法で、外部化手法の妥当性や有効性に関する疑問点・問題点が冒頭の引用です。
インデックス付き圏 $`\cat{P}`$ は、$`\cat{C}`$ の適当なシード射／シード四角形のクラスに対してハイパードクトリンを定義するとします。このハイパードクトリンが、依存型理論または述語論理を展開する舞台となります。
現時点では、外部化しない手法も参考にしながらも、外部化手法は使い続けていこうと思っています。ただし、「最近の型理論： 外部化手法のもとでのパイ型と指数型」で仮定したフル外延性は強すぎる仮定なので、（フルとは限らない）外延性にまで弱めます。外延性も外してしまうと、外部化手法はうまく機能しなくなるでしょう。
具象圏と忘却関手
世界の幹の部分に“コア銀河＝集合圏”が居ます。しかし集合圏ではない銀河（非コアな銀河）も認めます。なぜなら、計算や証明のモデルとなる圏は集合圏とは限らないからです。対象が順序集合や位相空間や一貫性空間〈coherence space〉で、射は何らかの意味の“連続写像”である圏は、計算や証明のモデルに使われますが、集合圏ではありません。
とは言え、これらの圏は集合圏と関係しています。台対象〈underlying object〉は集合であり、射は写像として表現されます。一般に、対象が集合に何らかの構造を載せたモノで、射が構造を保存する写像であるような圏を具象圏〈concrete category〉といいます。対象／射に台集合／台写像を対応させる忘却関手は忠実関手になります。
注意： この節内で使っている $`U, U'`$ は宇宙とその後者宇宙ではなくて、忘却関手とその変形です。後から気付いたけど、記号の偶発的バッティングが起きてます。
$`\cat{C}`$ が具象圏で、$`U:\cat{C} \to {\bf Set} \In {\bf CAT}`$ は忘却関手とします。集合 $`X \in |{\bf Set}|`$ に対して、
$`\quad U^{-1}(X) := \{ A \in |\cat{C}| \mid U(A) = X \}`$
は、空集合かも知れないし、大きなクラスになるかも知れません。$`U^{-1}(X)`$ が空でないなら、それは集合 $`X`$ に載る構造全体のクラスになります。例えば、自然数の集合 $`{\bf N}`$ に載るモノイド構造の全体とかです。
具象圏の忘却関手は、対象クラス $`|\cat{C}|`$ 上で単射とは限りません。したがって、埋め込み関手とは限りません。しかし、次のように変形すると、対象クラス上で単射〈injective-on-objects〉になります。
$`\text{For }X \in |\cat{C}|\\
\quad U'(A) := \{A\} \times U(A) \;\in |{\bf Set}|`$
圏の対象でタギングしたタグ付き集合にするわけです。
変形した忘却関手 $`U'`$ は、もとの忘却関手 $`U`$ が持っていた有意義なファイブレーション構造を壊してしまいますが、集合圏への埋め込み関手になります。$`U'`$ による埋め込み像 $`\mrm{Img}(U') \subseteq {\bf Set}`$ は集合圏の部分圏です。像圏 $`\mrm{Img}(U')`$ は、もとの対象／射の構造や特徴は忘却してますが、圏全体としての大域的形状は保存しています。
我々が扱いたい銀河とは、忘却埋め込みを備えた具象圏だと考えていいでしょう。つまり、コア銀河のなかに形状を保存して展開できるような圏です。コア銀河の部分圏としての形状から、当該の非コア銀河の情報が得られます。一般の銀河 $`\cat{C}`$ は集合圏（コア銀河）にある程度似ている、と言えます。
外延的引き戻し付きデカルト閉圏と内部圏
外部化と内部化の話をするために、もう少し準備をします。
次の関手達は、本記事最初の節で説明しました。
$`\quad \ol{(\hyp)}\; = \mrm{Inst} : \cat{C} \to {\bf Set}\\
\quad \J : \cat{C} \to {\bf Cat}\\
\quad \J : \cat{C} \to {\bf CAT} \:\text{ （同じ名前をオーバーロード）}
`$
外延化関手 $`\mrm{Inst}`$ が忠実関手のとき、圏 $`\cat{C}`$ は外延的〈extensional〉と呼びます（「最近の型理論： 外部化手法のもとでのパイ型と指数型」で導入）。対象の外延化の定義
$`\text{For } A\in |\cat{C}|\\
\quad \ol{A}\; := \cat{C}({\bf 1}, A)`$
から、$`A \mapsto \ol{A}\;`$ は単射になります。通常の圏の定義では、ホムセットは交わらないからです（「ホムセットは交わるのか」参照）。したがって、$`\cat{C}`$ が外延的なら外延化関手は埋め込み関手になります。
外延的圏 $`\cat{C}`$ に対して、外延化関手による埋め込み像を $`\mrm{Extern}(\cat{C})`$ と書いて、$`\cat{C}`$ の外部化と呼びます。$`\mrm{Extern}(\cat{C})`$ は集合圏の部分圏になります。似た言葉（同じ言葉でもいいかも）を使ってますが、圏の対象の外延化（集合化）ではなくて、圏全体を集合と写像で表現するのが外部化です。混乱の心配がなければ、圏の外部化も（対象／射の外延化と同じく） $`\ol{\cat{C}}`$ と書きます。
$`\cat{C}`$ がデカルト閉圏のとき、そのデカルト閉構造は $`\ol{\cat{C}}`$ にも反映されます。つまり $`\ol{\cat{C}}`$ は、デカルト閉構造も含めて $`\cat{C}`$ のレプリカ〈代理複製物〉になっています。
さて、引き戻し〈プルバック | ファイバー積〉を持つデカルト閉圏 $`\cat{C}`$ を（そのまんま）引き戻し付きデカルト閉圏と呼ぶことにします。等化子〈イコライザー〉があればファイバー積を作れるので、等化子付きデカルト閉圏でも同じことです。
圏 $`\cat{C}`$ がファイバー積を備えていれば、内部圏〈internal category〉を構成できます。$`\cat{C}`$ の内部圏と内部関手の全体からなる圏を $`\mrm{Cat}(\cat{C})`$ とします。1-圏である（2-射までは考えてない）ことを強調するなら $`\mrm{Cat}^1(\cat{C})`$ と書きます。
引き戻し付きデカルト閉圏 $`\cat{C}`$ が外延的でもある（外延的引き戻し付きデカルト閉圏）とします。この状況で、内部圏 $`\cat{A}\in |\mrm{Cat}(\cat{C})|`$ は、$`\cat{C}`$ の外部化を通じて、圏 $`\ol{\cat{C}}`$ の内部圏へと外部化できます。ところが、$`\ol{\cat{C}}`$ は集合圏の部分圏だったので、外部化された $`\cat{A}`$ は通常の圏となります。
記号のオーバーロードがヘビーになりますが、外部化された $`\cat{A}`$ も $`\ol{\cat{A}}`$ とします。まとめると：
- $`\cat{A} \in |\mrm{Cat}(\cat{C})|`$ ： $`\cat{A}`$ は、 $`\cat{C}`$ の内部圏
- $`\ol{\cat{A}} \in |\mrm{Cat}(\ol{\cat{C}})|`$ ： $`\ol{\cat{A}}`$ は、 $`\cat{C}`$ の外部化である $`\ol{\cat{C}}`$ の内部圏
- $`\ol{\cat{A}} \in |\mrm{Cat}({\bf Set})|`$ ： $`\ol{\cat{A}}`$ は、 集合圏の内部圏（通常の圏）
圏 $`\cat{C}`$ も、$`\cat{C}`$ の内部圏であった $`\cat{A}`$ も、外部化することにより共通の環境 $`{\bf Set}`$ 内に同列に存在できます。外部化は、階層性を解除する働きがあります。
メタ巡回性と外部化・内部化
計算や証明のモデル化では、「自分のなかに自分が埋め込まれている」ような状況に遭遇します。このような状況は、「メタ巡回性」、「自己言及」、「非可述性」、「再帰」、「ゲーデル化」、「フラクタル」などのキーワードで語られることがあります。
バエズ〈John C. Baez〉は、このような状況をスノーグローブに例えています。
雪が降る景色のなかにある模型の家は、模型そっくりなホントの家の机に上に置いてあるのです。このスノーグローブを眺めることは、本物の家を“家の外から”眺めることと同じです。
あるいは、「そっくりハウス」（谷山浩子）のジャケットの絵が同じ状況を描写しています。
女の子が見ている家は、この子が居る家です。
「自分のなかに自分が埋め込まれている」ことを素朴集合論の概念・記法で書けば $`x \in x`$ です。これは矛盾を導くから排除すべきとされていますが、それが必要なことはよくあります。
このような“スノーグローブ現象”は、僕にとって興味の対象でもあり悩みのタネでもありました。
- ブログ内で「スノーグローブ」の検索結果
記事をひとつ*5と、そこから参照さている記事を挙げれば：
上記過去記事にて、メタ巡回構造や万能対象*6の話をした後に幾分あきらめたような物言いをしています。
スノーグローブ現象が起きると、インスタンスレベルとメタレベルが混じり合うわけですが、エルブラン風のモデルの作り方をすると、さらに構文領域と意味領域も混じってきて、なんだか混沌としたスープ状の奇妙な構造物を相手にすることになります。奇妙と感じるのは我々に先入観があるからで、計算モデルの世界はそんなもんなのかも知れません。
スノーグローブ現象のメカニズムを明晰に理解することは難しいですね。
「圏 $`\cat{C}`$ のなかに圏 $`\cat{C}`$ が埋め込まれている」こともスノーグローブ現象ですが、外延化による外部化と内部圏を使えば、ある程度は説明できるかも知れません。
$`\cat{C'}`$ は外延的引き戻し付きデカルト閉圏 $`\cat{C}`$ の内部圏だとします。$`\cat{C'}`$ が、$`\cat{C}`$ を“内部化した圏”だとすれば、内部圏 $`\cat{C'}`$ は $`\cat{C}`$ とソックリな複製なので、「圏 $`\cat{C}`$ のなかに圏 $`\cat{C}`$ が埋め込まれている」と言えるでしょう。
ところが、“内部化”の定義はまだありません。“ソックリ”が何を意味しているかも不明です。次のように考えましょう。
- 内部圏 $`\cat{C'} \in |\mrm{Cat}(\cat{C})|`$ が、通常の圏 $`\cat{D}`$ の内部化であるとは、$`\cat{C'}`$ の外部化が $`\cat{D}`$ であること。つまり、$`\ol{\cat{C'}}\; = \cat{D}`$ 。
- 2つの圏がソックリであるとは、それらが圏同値であること。
この定義を採用すると、「内部圏 $`\cat{C'}`$ は $`\cat{C}`$ とソックリ」であることは次のように書けます。
$`\quad \ol{\cat{C'}}\, \simeq \cat{C}`$ （$`\simeq`$ は圏同値とする）
サイズ（集合論的基数）が著しく違った圏でも圏同値にはなれるので、集合論的矛盾は回避できそうです。そうは言っても、親の圏と圏同値になるような内部圏を構成するのは簡単じゃないでしょうが。
それでもともかく、外部化・内部化を使う準備はある程度できました。
*1:集合論の話に翻訳すると、到達不能基数〈{strongly}? inaccessible cardinal〉がいくらでも存在する、ということらしいです。集合論では、異常ではなくて普通なのかも知れません。
*2:極限・余極限の構造を備えた圏をスケッチ〈sketch〉と呼びます。
*3:バエズ〈John C. Baez〉が説明に使っていた絵、出典不明
*4:画像は https://www.amazon.co.jp/dp/B00006II9F より
*5:もうひとつ挙げるなら、手塚治虫の『火の鳥』の世界観に触れた「手塚治虫とデカルト閉圏」かな。
*6:万能対象の持つ特徴のひとつは reflexive object であることです。
