ダラッっと語る。$`\newcommand{\In}{\text{ in }}
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\Imp}{\Rightarrow}
%\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{ \mathrm{op} }
\newcommand{\hyp}{\text{－} }
\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\newcommand{\Vtimes}{\mathop{!\!{\times}} }
`$
内容：
色々な型理論的圏
タイトルに「依存型理論」と書きましたが、現在の型理論は、マーチンレフ〈Per Erik Rutger Martin-Löf | マルティンレーフ〉に端を発する依存型理論の系譜上にあり、単に「型理論」と言ってもそれは依存型理論のことでしょう。依存性を扱わない型理論が無意味というわけではないですが、現実的問題だと依存性無しでは表現力が不足なことが多いです。
依存型理論を圏論ベースで展開するとして、どんな方式・流儀があるでしょうか？ これについては、「依存型理論の圏論的セマンティクスの資料」で紹介したnLabの記事がよくまとまっています。
- [nLab]
- Title: categorical semantics of dependent type theory
- Authors: nLab authors
- Date: Last revised on June 6, 2024
- URL: https://ncatlab.org/nlab/show/categorical+semantics+of+dependent+type+theory
このnLab記事に、型理論のための圏として、次のような圏（の種別）が挙げられています。
- 包括圏〈comprehension category〉
- ディスプレイクラス付き圏〈display map categories | category with display class〉
- 属性付き圏〈category with attributes | CwA〉
- ファミリー付き圏〈category with families | CwF〉
- 自然モデル〈natural model〉
- 表現可能射付き圏〈category with representable maps〉*1
- C-システム〈C-system〉
このなかで、僕が使おうとしているのはヴォエヴォドスキーのC-システム〈C-system〉です。C-システムは、カートメルのコンテキスト圏〈contextual category〉と同じものです。ヴォエヴォドスキーが用語「圏」を使いたくない事情（「パチモンの圏 ＝ システム」参照）は納得できるので「C-システム」と呼びます。
C-システムは、属性付き圏〈CwA〉にカートメルツリー構造を入れたものです。属性付き圏は、ホフマン〈Martin Hofmann〉*2が考案したのかと思っていたのですが、違いました。属性付き圏もカートメルです。ホフマンは、学位論文（下）で属性付き圏を使った人で、属性付き圏の“使い手”ですが、“創始者”ではありません。
- [Hof95]
- Title: Extensional concepts in intensional type theory
- Author: Martin Hofmann
- Date: 1995
- Pages: 300p
- URL: https://ncatlab.org/nlab/files/HofmannExtensionalIntensionalTypeTheory.pdf
nLabで "display map categories" と呼ばれている圏は、ディスプレイ射のクラスが付随した圏ということでディスプレイクラス付き圏〈category with display class〉と僕は呼んでいます。ディスプレイクラスという概念は、C-システムを定義する際も使っています。型理論的圏には、なんらかの意味のディスプレイクラスが下部構造に入り込んでいるようです。そのことは以下の過去記事で書いています。
型理論的圏達を鳥瞰的〈bird's eye view〉に眺める場合は、ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉が便利です。包括圏は抽象度が高い構造で、様々な型理論的圏を取り込むことが可能です。包括圏は、以下の図式として定義できます。
$`\quad \xymatrix@C+2pc{
{}
&{\cat{C}}
\\
{\cat{E}} \ar[ur]^{\mrm{Ext}} \ar[dr]_{\mrm{Proj}} \ar[r]|-{\mrm{Comph} }
& {\mrm{Arr}(\cat{C})} \ar[u]_{\mrm{Dom}} \ar[d]^{\mrm{Cod}}
\\
{}
& {\cat{C}}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
条件は：
- $`\cat{E} \overset{\mrm{Proj}}{\to} \cat{C}`$ はファイブレーション〈ファイバー付き圏〉である。
- 包括演算／関手〈comprehension {operator | functor}〉$`\mrm{Comph}`$ の射パートは、デカルト射を保存する（下の図）。
$`\quad \xymatrix{
{\mrm{Cart}(\mrm{Proj})} \ar@{^{(}->}[d] \ar[r]^{ \mrm{Comph'} }
&{\mrm{Cart}(\mrm{Cod}) } \ar@{^{(}->}[d]
\\
{\mrm{Mor}( \cat{E}) } \ar[r]_{ \mrm{Comph} }
&{\mrm{Mor}(\mrm{Arr}(\cat{C}) ) }
}\\
\quad \text{commutative }\In \mbf{SET}
`$
ここで、$`\mrm{Cart}(\hyp)`$ は関手（圏バンドル）のデカルト射の集合（「集合のバンドルと圏のバンドル」参照）です。$`\mrm{Cart}(\mrm{Cod})`$ は、圏 $`\cat{C}`$ のプルバック四角形の集合 $`\mrm{PBSq}(\cat{C})`$ のこと（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）なので、包括圏の包括演算の値は、プルバック四角形になります。
包括圏の定義は、初見では「なに言ってるんだ？」ですが、他の型理論的圏の定義をパッキングする（抽象的にまとめる）と確かに包括演算に帰着します。
「集合のバンドルと圏のバンドル // 例： 包括圏」でも包括圏の説明をしてますが、記号を変えているので対応を示します。
| この記事 | 過去記事 |
|---|---|
| $`\mrm{Proj}`$ | $`P`$ |
| $`\mrm{Arr}(\cat{C})`$ | $`\mrm{Bun}(\cat{C})`$ |
| $`\mrm{Comph}`$ | $`\mrm{Ext}`$ |
| $`\mrm{Ext}`$ |
$`\mrm{Ext}`$ の使い方が変わっているので注意してください。$`\mrm{Arr}(\cat{C}) = \mrm{Bun}(\cat{C})`$ であることは「アロー圏 ＝ バンドルの圏」に書いています。
パルムグレンの包括圏
[追記]見出しが誤解を招く文言だったかな。包括圏という概念はジェイコブスによるものです。パルムグレンの包括圏は、パルムグレンによる複前層の圏から作った包括圏の具体事例のつもりです。「パルムグレン圏」のほうがよかったかも知れない。[/追記]
「パルムグレンによる、型理論の複前層モデル」でパルムグレンの複前層の圏 $`\mrm{MPSh}(\cat{C})`$ を紹介しました。ヴォエヴォドスキーの、宇宙圏から構成するC-システムは、パルムグレンの複前層の一般化になっています。パルムグレン／ヴォエヴォドスキーのことは次の記事で書いています。
パルムグレン／ヴォエヴォドスキーの論文を再掲すると：
- [Pal13-16]
- Title: The Grothendieck construction and models for dependent types
- Author: Erik Palmgren
- Date: March 8, 2013; minor editing May 28, 2016
- Pages: 23p
- URL: https://staff.math.su.se/palmgren/iterated_presheaves_and_dependent_types_v8.pdf
- [Voe14-15]
- Title: A C-system defined by a universe category
- Author: Vladimir Voevodsky
- Submitted: 28 Sep 2014 (v1), 29 Jul 2015 (v3)
- Pages: 33p
- URL: https://arxiv.org/abs/1409.7925
パルムグレンの複前層の圏 $`\mrm{MPSh}(\cat{C})`$ を、すべての圏 $`\cat{C}`$ に渡って寄せ集めると興味深い圏を作れそうです。グロタンディーク構成の記法で書けば次のようです。（$`\mbf{Cat1}`$ は2-圏ではなくて、圏達の1-圏。）
$`\quad \mbf{MPSH} := {\displaystyle\int_{ \mbf{Cat1} } \mrm{MPSh}(\hyp) } =
\int ( \mbf{Cat1} \mid \mrm{MPSh}(\hyp))`$
$`\mbf{MPSH}`$ について書いたことはまだないのですが、おそらく次のようにしても作れます。
- 小さい圏 $`\cat{C}`$ に対して、$`\mrm{Step}(\cat{C}) := |[\cat{C}^\op, {\bf Set}]|`$ と定義する。$`\mrm{Step}(\cat{C})`$ は、$`\cat{C}`$ 上の前層の集合になる（射を入れてないので圏にはならない）。
- $`\mrm{Step}(\hyp)`$ を、圏 $`\mbf{Cat1}`$ 上の関手にまで拡張すると、$`\mrm{Step}(\hyp)`$ は $`\mbf{Cat1}`$ 上の前層となる。ただし、値を $`\mbf{SET}`$ にとる前層。
- 前層のグロタンディーク構成（要素の圏） $`\int ( \mbf{Cat1} \mid \mrm{Step}(\hyp))`$ を作る。
いずれにしてもグロタンディーク構成なので、次のようなファイブレーションができます。
$`\quad \mrm{Base} : \mbf{MPSH} \to \mbf{Cat1} \In \mbf{CAT}`$
このファイブレーションに対して拡張包括構造を定義することによって、$`\mbf{MPSH}`$ は包括圏となるでしょう（C-システムになりそう）。この包括圏は、非常に重要なものだと思われます。まだちゃんと調べてないのですが、パルムグレン／ヴォエヴォドスキーの論文に書いてある内容かも知れません。
ν-インスティチューション
型理論とインスティチューションの関係は、例えば次の過去記事で述べています。
インスティチューションは抽象的過ぎて、具体例を作るときにやることが多すぎる、というのが僕の不満です。具体例を作るときに必要なメカニズムをある程度備えたインスティチューションを半具象インスティチューション〈semi-concrete institution〉と過去記事で呼びました。
インスティチューションの変種にπ-インスティチューション（「演繹系と閉包系」参照）なんてのがありますから、半具象インスティチューションを、ギリシャ文字を先頭に付けてν-インスティチューション〈ν-institution〉と呼ぶことにします。'ν' は "new" の意味を含んでいます。
ν-インスティチューションは、包括圏のあいだの包括構造を保つ関手だと定義できます。どうしてこれが具象性を持ったインスティチューションの定義になるのか？ その根拠は以下の過去記事にあります。
インスティチューションの指標の圏 $`\cat{S}`$ は、型理論的なコンテキストの圏 $`\cat{C}`$ の反対圏だと思ってよいのです。インスティチューションのモデル空間関手 $`M`$ は、$`\cat{S}`$ 上の反変関手なので、$`\cat{C}`$ 上の共変関手です。共変関手が、拡張包括構造（に登場するプルバック四角形）を保つならば、インスティチューションの充足関係が定義できます。
この事情があるので、型理論／型システムの構文圏〈{syntax | syntactic} category〉$`\cat{C}`$ （対象をコンテキストと呼ぶ）から、意味論的ターゲット圏 $`\cat{T}`$ へのプルバック保存関手 $`M`$ があれば、$`\cat{S} = \cat{C}^\op`$ 上にインスティチューションを構成できます。よって、$`(\cat{C}, \cat{T}, M)`$ がν-インスティチューションだと言っても差し支えありません。
型理論／型システムの構文圏として、包括圏を考えれば十分な一般性があります。意味論的ターゲット圏も、圏の種別〈ドクトリン〉としては、構文圏と同じく包括圏だとします。包括圏達を対象として、適切な1-射と2-射を備えた2-圏を $`\mbf{ComphCAT}`$ とします。ν-インスティチューションとは、圏 $`\mbf{ComphCAT}`$ の射に過ぎないことになります。
$`\quad M:\cat{C} \to \cat{T} \In \mbf{ComphCAT}`$
$`\mbf{ComphCAT}`$ は2-圏なので、そのホム空間は1-圏となります。
$`\quad \mbf{ComphCAT}(\cat{C} , \cat{T}) \;\in |\mbf{CAT}|`$
このホム1-圏は、同一の指標圏 $`\cat{S} = \cat{C}^\op`$ 上のインスティチューション達の圏となります。
ところで、インスティチューションのモデル空間関手が値をとるターゲット圏で標準的〈standard〉なものは何でしょうか？ おそらく $`\mbf{MPSH}`$ でしょう。デフォルトのターゲット圏として $`\mbf{MPSH}`$ を選べば、次のように書けます。
$`\quad \nu\mbf{Insttt}[\cat{S}] := \mbf{ComphCAT}(\cat{S}^\op , \mbf{MPSH}) \;\in |\mbf{CAT}|`$
$`\nu\mbf{Insttt}[\cat{S}]`$ は、指標圏 $`\cat{S}`$ 上のすべてのν-インスティチューションからなる圏です。
ダラッの続きは？
$`\mbf{MPSH}`$ をC-システムとして定義するのは面白いし重要でしょう。長さ 0 のパルムグレンの複前層 $`(\cat{C} \mid )`$ は、$`\mbf{MPSH}`$ のなかでは長さ 1 になります。$`\mbf{MPSH}`$ のなかの長さ 0 の対象は、ほんとに何もない絶対的な空になります。$`\mrm{MPsh}(\cat{C})`$ は、$`\mbf{MPSH}`$ に埋め込まれることになります。
$`\mrm{MPsh}(\cat{C})`$ や $`\mbf{MPSH}`$ は、小さい圏 $`\cat{C}`$ をベースとして定義していますが、「小さい」の制限を外すと、$`\mrm{Step} : \mbf{Cat} \to |{\bf SET}|`$ を複前層（長さ 1 だけど）として扱えます。「サイズが大きい世界で自分自身を内省する」ことになるので、スノーグローブ現象／マイクロコスモ原理が現れます。
$`\mrm{Step}(\hyp)`$ は、集合を値とする前層として定義しましたが、圏を値とするインデックス付き圏とすれば $`\mrm{Step}(\hyp)`$ を一般化できます。グロタンディーク構成は、（前層でなくても）インデックス付き圏に対して実行できるので、同じ議論ができます。複雑性が増して晦渋になりますが、応用範囲は広がります。
C-システムに出てくるカートメル構造は、圏に対して脱着可能な構造です。包括圏に必ずカートメル構造が入るとは限りませんが、ヴォエヴォドスキーの意味での宇宙から生成される圏にはカートメル構造が入ります。圏のカートメル構造は、対象が再帰的・有限的に構成可能なことを表しています。ツリー以外のカートメル構造とか、どのような圏にカートメル構造が入るか？ を考えるのは意味があるでしょう。また、カートメル構造付きの同型とカートメル構造を抜いたときの同型の関係も興味あります。
以下の記事では、球体集合の構文表示を扱いました。
形式体系〈形式的演繹形〉の導出により図形を表示できる、というのは実は一般的な現象のような気がします。“図形”という概念が、Diag構成（「Diag構成： 圏論的構成法の包括的フレームワークとして」参照）の意味でのダイアグラム〈図式〉と繋がるかも知れません。
*1:上村太一さんによる理論です。
*2:https://www.cis.upenn.edu/~bcpierce/papers/MartinHofmannMemorial.pdf によると、"1965 Born in Erlangen, Germany" "2018 died in Japan" 、日本で亡くなったようです。
