タイトルの件に関して、とりあえず概要だけ述べます。おおよそのストーリーを語るので、細部の抜けやギャップはあります。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\J}{\mathrm{J}}
\newcommand{\In}{\text{ in }}
\newcommand{\hyp}{ \text{－} }
`$
内容：
シリーズ・ハブ記事：
はじめに
「階層化された宇宙達を備えた型理論」のヨーガ〈基本教義〉は、
- 型は宇宙の要素である
です。が、「宇宙より銀河」（「最近の型理論： 型理論の構文論と意味論」参照）というキャッチフレーズにより、我々は以下の解釈を採用します。
- 型は銀河（という圏）の対象である
銀河はデカルト閉圏だとすれば、単純型理論〈simple type theory〉や命題論理〈propositional logic〉（の連言含意フラグメント）を銀河内で展開できます。型ファミリーの概念を導入すると、依存型理論〈dependent type theory〉ができます。依存型理論の論理的対応物が述語論理〈predicate logic〉です。
述語論理の圏論的定式化にはローヴェア〈William Lawvere〉のハイパードクトリン〈hyperdoctrine〉があります。ハイパードクトリンは、依存型理論の枠組みでもあります。カリー／ハワード／ランベック対応により、“単純型理論←→命題論理”、“依存型理論←→述語論理”と対応するので、依存型理論と述語論理が共通のフレームワークに包摂されるのは当然とも言えます。
適当なセッティングのもとで、依存型理論を目指してシステムを構成すれば、そのシステムは述語論理にも使える／使えてしまう、というわけです。この“依存型理論・兼・述語論理”のシステムの公理的特徴付けがハイパードクトリンです。ハイパードクトリンの具体的構成には、“ファミリー＝述語”の圏における極限・余極限、カン拡張を使います。
記法の約束
「一般化されたファミリーの圏」と同じ記法の約束をします。サイズのランク〈レベル〉をr、次元をnとして、サイズランクrのn-圏達の(n + 1)-圏を次のように書きます。dはデフォルトのランクです。
| $`r = d `$ | $`r = d + 1`$ | |
| $`n = 0`$ | $`{\bf Set}`$ | $`{\bf SET}`$ |
| $`n = 1`$ | $`{\bf Cat}`$ | $`{\bf CAT}`$ |
| $`n = 2`$ | $`{\bf 2Cat}`$ | $`{\bf 2CAT}`$ |
サイズ・ランクによる階層（表の横方向）はグロタンディーク宇宙の階層に起因します。それについては、次の記事を見てください。
$`\cat{C}, \cat{D}`$ が圏のとき、関手圏を $`[\cat{C}, \cat{D}]`$ と書きますが、指数記法 $`\cat{D}^\cat{C}`$ も使います。関手圏のホムセットを書くときは、指数記法のほうが視認性が良いようです。
$`\quad \cat{D}^\cat{C}(F, G)`$ ： 関手圏のホムセット（自然変換の集合）
カン拡張は、$`\mrm{Ran}_K(F), \mrm{Lan}_K(F)`$ （右, 左）と書きます。
型圏化
デカルト圏 $`\cat{C}`$ は宇宙 $`U = |{\bf Set}|`$ に対して局所小圏だとします。これは次の意味です。
- $`|\cat{C}|\subseteq |{\bf Set}|`$
- $`\forall A, B \in |\cat{C}|.\, \cat{C}(A, B) \in |{\bf Set}|`$
「最近の型理論： 宇宙と世界、そして銀河」で次の定義をしています。
$`\quad \mrm{Inst}(A) := \cat{C}({\bf 1}, A)`$
これは、型 $`A`$ のインスタンス〈instance〉全体の集合です。「デカルト閉・型システム」でも同じ定義をしてますが、型 $`A`$ の外延化〈extensionalize〉と呼んでいます。つまり、次の2つは同じ集合です。
- 型 $`A`$ のインスタンス全体の集合
- 型 $`A`$ の外延化〈extensionalize〉
デカルト圏 $`\cat{C}`$ の対象 $`A`$ に対して、$`\mrm{Inst}(A) \in |{\bf Set}|`$ は集合ですが、集合は離散圏とみなせます。離散圏とみなした $`\mrm{Inst}(A)`$ を $`\J(A)`$ と書くことにします。以下の $`\mrm{Disc}`$ は、集合を離散圏にする関手です。
$`\quad \J(A) := \mrm{Disc}(\mrm{Inst}(A)) = (\text{set }\cat{C}({\bf 1}, A)\text{ as discrete category})`$
$`f:A \to B \In \cat{C}`$ に対して、離散圏のあいだの関手 $`\J(f): \J(A) \to \J(B) \In {\bf Cat}`$ を簡単に定義できるので、$`\J`$ は次のような関手です。
$`\quad \J: \cat{C} \to {\bf Cat}`$
$`\cat{C}`$ は1-圏で、$`{\bf Cat}`$ は2-圏ですが、1-圏を2-離散2-圏（2-射が恒等2-射だけの2-圏）とみなせば：
$`\quad \J: \cat{C} \to {\bf Cat} \In {\bf 2CAT}`$
デカルト圏 $`\cat{C}`$ が銀河ならば、その対象 $`A`$ は型です。$`\J(A)`$ は型を圏とみなしたものです。このことから、関手 $`\J`$ あるいは関手の値 $`\J(A)`$ を型圏化〈type categorification〉と呼ぶことにします。
「依存型と総称型の圏論的解釈」では、$`\J`$ を反レイフィケーション〈dereification〉と呼んでましたが、ちょっと分かりにくい言葉なので、型圏化に置き換えました。
型圏化を前提にすれば次のように言えます。
- 型は圏〈銀河〉の対象だが、それ自体が圏である。
相対的完備性
「依存型と総称型の圏論的解釈」で、自己完備〈self complete〉な圏という概念を導入しています。ここでは、自分自身だけではなく、他の圏に対して相対的に完備という概念を導入します。
$`\cat{C}`$ は前節と同じとして、$`\cat{D}`$ をもう1つの局所小圏とします。$`\cat{C} = \cat{D}`$ でもかまいません。圏 $`\cat{D}`$ が$`\cat{C}`$-完備〈$`\cat{C}`$-complete〉とは次のことです。
- 任意の対象 $`A\in |\cat{C}|`$ に対して、任意の関手 $`F:\J(A) \to \cat{D} \In {\bf CAT}`$ は極限を持つ。
$`\cat{C} = \cat{D}`$ のときは自己完備になります。
圏 $`\cat{D}`$ が$`\cat{C}`$-余完備〈$`\cat{C}`$-cocomplete〉も同様に定義します。圏 $`\cat{D}`$ が$`\cat{C}`$-完備かつ$`\cat{C}`$-余完備のとき、$`\cat{C}`$-両完備〈$`\cat{C}`$-bicomplete〉といいます*1。
局所小デカルト圏 $`\cat{C}`$ と、$`\cat{C}`$-両完備な圏（これも局所小圏） $`\cat{D}`$ があると、それをもとにハイパードクトリンを作れます。つまり、依存型理論／述語論理が出来ることになります。
ファミリーのインデックス付き圏
$`\cat{C}, \cat{D}`$ は前節のセッティング（$`\cat{D}`$ が$`\cat{C}`$-両完備）だとします。$`A\in |\cat{C}|`$ に対して、次の関手圏を考えます。
$`\quad {\bf CAT}(\J(A), \cat{D}) \in |{\bf CAT}|`$
$`\cat{D}`$ が小さいとは仮定してないので（局所小は仮定しているけど）、$`\cat{D}\in |{\bf Cat}|`$ は言えません。$`\J(A) \in |{\bf Cat}|`$ は確実ですが、$`{\bf Cat}\subset {\bf CAT}`$ （部分2-圏）なので、$`\J(A) \in |{\bf CAT}|`$ とみなしています。
この関手圏は次のようにも書くのでした。
$`\quad \cat{D}^{\J(A)} = [\J(A), \cat{D}] = {\bf CAT}(\J(A), \cat{D}) \in |{\bf CAT}|`$
$`\cat{D}^{\J(A)}`$ よりもっと短く書けるように、次の定義をします。
$`\quad \cat{P}[A] := \cat{D}^{\J(A)} \in |{\bf CAT}|`$
$`{\bf CAT}(\J(A), \cat{D}) \cong {\bf SET}(\mrm{Inst}(A), |\cat{D}|)`$ なので、圏 $`\cat{P}[A]`$ の対象はファミリー〈family〉、射はファミリーのあいだの準同型射〈homomorphism between families〉だと言えます。述語論理の文脈なら、圏 $`\cat{P}[A]`$ の対象は述語〈predicate〉で、射は証明〈proof〉です。
$`\cat{P}[\hyp]`$ は、$`\cat{C}, \cat{D}`$ から一意に決まりますが、これは $`\cat{C}`$ 上のインデックス付き圏〈indexed category〉（“圏の圏”への反変関手）にできます。$`f:A \to B \In \cat{C}`$ に対して、$`\J(f)`$ のプレ結合で逆向きの関手が誘導されます。
$`\quad \cat{P}[f] : \cat{P}[B] \to \cat{P}[A] \In {\bf CAT}`$
$`\cat{P}[f]`$ を $`\Delta_f`$ あるいは $`f^*`$ とも書きます。この定義により、$`\cat{P}[\hyp]:\cat{C}^\mrm{op} \to {\bf CAT}`$ です*2。
インデックス付き圏にはグロタンディーク構成ができるので、グロタンディーク平坦化圏とグロタンディーク・ファイブレーション（すぐ下）を構成できます。
$`\quad \pi : \int_\cat{C} \cat{P}[\hyp] \to \cat{C} \In {\bf CAT}`$
グロタンディーク構成については、例えば次の記事を参照してください。
射影と随伴トリプル系
$`X, A \in |\cat{C}|`$ として、第一射影 $`\pi^{X, A}_1 : X\times A \to X \In \cat{C}`$ を単に $`\pi^{X, A}`$ と書きます。$`X, A`$ が了解されているなら $`\pi`$ だけでもいいとします。適 当な $`X, A`$ に対して $`\pi^{X, A}`$ と書ける $`\cat{C}`$ の射を射影射〈projection morphism〉、あるいは単に射影〈projection〉と呼びます。$`\pi^{{\bf 1}, A}, \pi^{A, {\bf 1}}`$ も射影です。
$`\cat{C}`$ 上のハイパードクトリンは、$`\cat{C}`$ 上のインデックス付き圏ですが、射影に対しては随伴トリプル系が構成できることを要求します。次のようなことです。
- $`\pi : X\times Y \to X \In \cat{C}`$ は射影とする。
- $`\Delta_\pi : \cat{P}[X] \to \cat{P}[X \times Y] \In {\bf CAT}`$ に左随伴関手が存在する。（$`\Delta_\pi`$ を右随伴関手とする随伴系が存在する。）
- $`\Delta_\pi : \cat{P}[X] \to \cat{P}[X \times Y] \In {\bf CAT}`$ に右随伴関手が存在する。（$`\Delta_\pi`$ を左随伴関手とする随伴系が存在する。）
基本的な道具である、極限、随伴、カン拡張については、以下の記事達が参考になるかも知れません。
$`\Delta_\pi`$ は、関手 $`\J(\pi)`$ をプレ結合する関手 $`\J(\pi)^*`$ で与えられるので、随伴系のホムセット同型は次の形になります。
$`\quad
\cat{D}^{\J(X \times Y)}(F, J(\pi)^*(G) ) \cong
\cat{D}^{\J(X )}(\mrm{Lan}_{\J(\pi)}(F), G )\\
\quad
\cat{D}^{\J(X \times Y)}(J(\pi)^*(G), F) \cong
\cat{D}^{\J(X )}(G, \mrm{Ran}_{\J(\pi)}(F) )`$
特に、$`X = {\bf 1}, |\J({\bf 1})| = \{*\}`$ のときは次のようです。$`\pi`$ の代わりに $`!`$ と書いています。この場合、$`\mrm{Lan}`$ は余極限、$`\mrm{Ran}`$ は極限になります。
$`\quad
\cat{D}^{\J({\bf 1} \times Y)}(F, J(!)^*(G) ) \cong
\cat{D}^{\J({\bf 1} )}(\mrm{Lan}_{\J(!)}(F), G ) \cong
\cat{D}(\mrm{colim}_{\J(Y)}\, F, G(*) )
\\
\quad
\cat{D}^{\J({\bf 1} \times Y)}(J(\pi)^*(G), F) \cong
\cat{D}^{\J({\bf 1} )}(G, \mrm{Ran}_{\J(!)}(F) ) \cong
\cat{D}( G(*), \mrm{lim}_{\J(Y)}\, F)`$
次のような対応関係があります。
| カン拡張 | 依存型理論 | 述語論理 |
|---|---|---|
| 左カン拡張 | シグマ型 | 存在限量子 |
| 右カン拡張 | パイ型 | 全称限量子 |
このような対応関係については以下の過去記事に書いています。
インデックス付き圏 $`\cat{P}[\hyp]`$ が、射影に関して左右のカン拡張を持つことを確認する必要があります。$`\cat{D}`$ が$`\cat{C}`$-両完備であることを根拠にします。また、ハイパードクトリンであるためには、ベック／シュバレー条件も必要になります。ハイパードクトリンとベック／シュバレー条件については以下の記事に書いてあります。
「カン拡張」の「拡張〈extension〉」という言葉に惑わされないでください。「拡張」と呼び名がついているから拡張だとは限りません（名は体を表さない！）。依存型理論のパイ型／シグマ型、述語論理の存在限量子／全称限量子は、縮小・集約という感じで、拡張とは正反対です。可換図式で示された条件を満たす射のなかで最も典型的（普遍的）なものを、たままた「拡張」という名で呼んでいるだけです。拡張の実体が縮小かも知れません。
[/追記]
おわりに
冒頭に注意したように、このストーリーにはちょいちょい抜けがあります。細部を詰めないといけません。もし思惑通りならば、かなり使い勝手の良いフレームワークになると思います。
必要となる素材は、デカルト圏 $`\cat{C}`$ と$`\cat{C}`$-両完備な圏 $`\cat{D}`$ です。例えば、$`\cat{C} = \cat{D} = {\bf Set}`$ と取れます。$`\cat{D}`$ として二値ブール代数を圏とみなしたものも取れます。$`\cat{C}, \cat{D}`$ は集合圏の部分圏であることを要求してないので、ωCPOの圏とかも利用できます。
ハイパードクトリンのベースとなる $`\cat{P}[\hyp]`$ はインデックス付き圏なので、グロタンディーク構成ができます。これは大きなメリットで、$`\cat{C}, \cat{D}`$ からの構成物を単一の圏（平坦化圏）として扱えます。
ハイパードクトリンは意味論的な構造ですが、構文論との関係はまた別に論じるつもりです。
