圏論をベースに型理論を展開するアプローチがあります。このアプローチは圏論的型理論と言えるでしょう。とはいえ、現在の型理論において圏論を使わないことは考えにくいので、型理論＝圏論的型理論 だと言っていいでしょう。また、依存性を扱う依存型理論が主流*1ですから、型理論＝依存型理論 だとも言えます。結局、おおむね 型理論＝圏論的依存型理論 だということです。
圏論的依存型理論で用いる圏論は、必然的にファイバー付き圏論となります。ファイバー付き圏は、（圏の）ファイブレーションとも呼びます。ファイブレーションが、型理論の主要なツールであり、現在の型理論はファイブレーション的アプローチを採用していることになります。
ファイブレーション的アプローチにおいて、型理論の概念がどのように圏論的に定式化されるか？ ザッと眺めてみます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\u}[1]{\underline{#1}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
%\newcommand{\Imp}{\Longrightarrow} % for meta prop
\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\harto}{\rightharpoonup } % HARpoon TO
`$
内容：
「インスタンス」を「項」と呼ぶのはやめよう
最初に、言葉の問題をハッキリさせておきます。そうしないと、今回の話題を語るうえで支障があるからです。
ソフトウェアやプログラミング言語の話のなかで、「型」と「インスタンス」という言葉はよく出てきます。型理論では、「インスタンス」を「項〈term〉」と呼ぶことが、かなり広く合意された習慣になっています。例えば、"Types as Propositions, Terms as Proofs" という有名なキャッチフレーズのなかの term はインスタンスの意味です。
しかし、インスタンスを「項」と呼ぶのは、どう考えても辻褄があってません。辻褄があってないだけなら、「そう決めたんだから従おう」という態度にもなるのですが、弊害がある（問題を引き起こす）ので、僕は受け入れがたいです。ジョイアル〈Andre Joyal〉は、"Notes on clans and tribes" のなかで次のように書いています。
Remark 1.2.1. An element $`a : E`$ is often called a term by type theorists. But this terminology is incorrect, since the notion of term is syntaxical while the notion of element is semantical.
注意 1.2.1. 要素 $`a : E`$ は、型理論ではしばしば項と呼ばれます。しかし、項の概念は構文的であるのに対し、要素の概念は意味的であるため、この用語法は間違っています。
「項」は構文的対象物を表す一般的言葉なので、使うとすれば、「型項〈type term〉」「インスタンス項〈instance term〉」のように語尾に付けて、それが構文的対象物であることを強調すればいいでしょう。そのことは以下の過去記事（のひとつの節）でも書いています。
最近眺めたデ・ブール〈Menno de Boer〉の論文 "A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory" では、かなり苦し紛れ（と思える）用語法を使っています； 「型〈type〉と項〈term〉」という習慣的用法を守りながら、それが構文的対象物であることを強調するときは語尾に "expression" を付けるのです。
構文的対象物である型は type expression 、構文的対象物である項〈インスタンス〉は term expression です。日本語なら、「型式」と「項式」、あるいは「型表現」と「項表現」でしょうか？ 苦しいなー。こんな言い方は採用したくない。
少なくともここでは、インスタンスを「項」と呼ぶのはやめて、インスタンスは「インスタンス」と呼びます。構文的対象物であることを強調したいなら「インスタンス項」です。
型理論の基本概念
型理論の基本概念には次があります。
- コンテキスト〈context〉
- 型〈type〉
- 代入〈substitution〉
- インスタンス〈instance〉
これらは、ファイバー付き圏〈fibered category | グロタンディーク・ファイブレーション | Grothendieck fibration | ファイブレーション | fibration〉 $`\pi : \cat{E}\to \cat{C}`$ によって次のように定式化されます。
- コンテキストは、ベース圏 $`\cat{C}`$ の対象
- 型は、トータル圏 $`\cat{E}`$ の対象
- 代入は、ベース圏 $`\cat{C}`$ の射
- インスタンスの定式化は、流儀によって異なる。
インスタンスの定式化は人により違いが出るところで、ややこしいですね。以下、インスタンスにフォーカスして話をします。
ハープーン
インスタンスはある種の射と考えることができます。コンテキスト $`\Gamma`$ と型 $`B`$ を結ぶ射なので、次のように書きましょう。
$`\quad f: \Gamma \harto B`$
ここで、特殊な矢印記号はハープーン（銛矢印、LaTeXでは \rightharpoonup、XyJax では \ar@^{->}[r]）です。ハープーンの左〈根本〉はコンテキスト、右〈先端〉は型です。単なる射ではなくてインスタンス（特別な射）であることを示すためにハープーンを使うことにします。ハープーンは、「最近の型理論： 拡張包括構造を持ったインデックス付き圏」から使っている記法です。
依存型理論では、型はコンテキストと切り離すことができません。したがって、型 $`B`$ にコンテキストを添えて $`B@\Delta`$ と書くことにします。これは、「コンテキスト $`\Delta`$ における型 $`B`$〈type $`B`$ at a context $`\Gamma`$〉」という意味です。
$`B@\Delta`$ は依存ペア〈dependent pair〉です。依存ペアの特別な書き方はなくて、通常のペアと同じく $`(\Delta, B)`$ と書かれるのが普通ですが、ここではアットマークを使って書くことにします*2。
$`\quad B@\Delta = (\Delta, B)`$
型をアットマークを使って書くことにすれば、インスタンスは次のように書けます。
$`\quad f: \Gamma \harto B@\Delta`$
上の形のインスタンスの全体を $`\mrm{Inst}(\Gamma, B@\Delta)`$ と書くことにします。ハープーンを使った宣言の代わりに次のように書いても同じです。
$`\quad f \in \mrm{Inst}(\Gamma, B@\Delta)`$
インスタンスの集合 $`\mrm{Inst}(\Gamma, B@\Delta)`$ をファイバー付き圏 $`\pi : \cat{E}\to \cat{C}`$ のなかにどう位置づけるか？ ファミリー付き圏〈category with families〉や局所デカルト閉圏〈locally Cartesian closed category〉では、インスタンスをファイバー付き圏のトータル圏のなかに実現します。一方、コンテキスト圏／C-システムでは、インスタンスはベース圏のなかで取り扱うことになります。
ファイブレーション的型理論におけるインスタンス
ファイバー付き圏 $`\pi : \cat{E}\to \cat{C}`$ に、型理論で必要なメカニズムを付け足した構造を $`\cat{K}`$ と置きます。例えば、$`\cat{K}`$ は「テレスコープと包括クラン」で定義した包括クランだと考えることができます。$`\cat{K}`$ はファイバー付き圏〈ファイブレーション〉に基づく構造ですから、ファイブレーション的型理論〈fibrational type theory〉の舞台です。
ファイブレーション的構造 $`\cat{K}`$ の各部を、型理論の用語で次のように呼ぶのでした（前々節参照）。
- コンテキスト $`\mrm{Context}(\cat{K}) := |\cat{C}|`$
- 型 $`\mrm{Type}(\cat{K}) := |\cat{E}|`$
- 代入 $`\mrm{Subst}(\cat{K}) := \mrm{Mor}(\cat{C})`$
そして、$`\Gamma \in \mrm{Context}(\cat{K})`$ と $`B@\Delta \in \mrm{Type}(\cat{K})`$ に対して、インスタンス達の集合 $`\mrm{Inst}_\cat{K}(\Gamma , B@\Delta)`$ が決まります。集合 $`\mrm{Inst}_\cat{K}(\Gamma , B@\Delta)`$ がどこに居るのかは、前節で述べたように流儀によります。
- 流儀1： $`\mrm{Inst}_\cat{K}(\Gamma , B@\Delta) \subseteq \mrm{Mor}(\cat{E})`$
- 流儀2： $`\mrm{Inst}_\cat{K}(\Gamma , B@\Delta) \subseteq \mrm{Mor}(\cat{C})`$
流儀2を採用するなら、インスタンスは次のように書けます。
$`\quad f: \Gamma \to \Delta\cdot B \In \cat{C}`$
つまり、流儀2のもとでは、次のように定義します。
$`\quad \mrm{Inst}_\cat{K}(\Gamma , B@\Delta) = \cat{C}(\Gamma, \Delta\cdot B)`$
流儀1であれ流儀2であれ、重要なことはインスタンスの“射影への分解”ができることです。それは、概念的には以下の図のようなものです。
$`\quad \xymatrix{
{A@\Gamma} \ar@{.}[r]
& {B@\Delta} \ar@{.}[d]
\\
\Gamma \ar[r]_{\varphi} \ar@^{->}[ur]^{f} \ar@^{->}[u]^q
& \Delta
}`$
ここで、$`\varphi`$ が $`f`$ の第一射影〈first projection〉（または{水平 | 横}射影〈horizontal projection〉）で、$`q`$ が第二射影〈second projection〉（または{垂直 | 縦}射影〈vertical projection〉）です。射影の作り方は流儀・メカニズムによりますが、次が成立します。
- $`\varphi \in \cat{C}(\Gamma, \Delta)`$
- $`q \in \mrm{VInst}_\cat{K}(\Gamma, A@\Gamma)`$
第二射影 $`q`$ はインスタンスですが、$`q`$ をさらに射影分解した第一射影は $`\mrm{id}_\Gamma`$ です。第一射影が恒等射となるインスタンスを垂直インスタンス〈vertical instance〉と呼ぶことにして、垂直インスタンス達の集合を $`\mrm{VInst}_\cat{K}(\Gamma, A@\Gamma)`$ と書いています。
結局、任意のインスタンスは、ベース圏 $`\cat{C}`$ の射（型理論の言葉では代入）と、垂直インスタンスに一意的に分解できます。この分解は、デカルト圏において、$`f:A \to B\times C`$ が2つの射影〈成分〉に分解できることの一般化になっています。
なお、「射影」という言葉はひどい曖昧多義語なので注意してください。曖昧性は「型理論に出てくる第一射影と第二射影」、「型理論で出てくる射影の整理と約束」にまとめてあります。
型理論の種別によっては、$`\cat{C}`$ の任意の射がインスタンスになる場合もあります。そのときは、垂直インスタンス、あるいは終対象からのインスタンスに限って「インスタンス」（習慣として「項」かも知れない）と呼ぶ、といった用語法もあります。ここは、型理論ごとの約束事を確認する必要があります。
