型理論の「インスタンス」の意味がハッキリしないのですが、次の3種にわければだいたい説明が付きそうです。
- 一般インスタンス
- ポインティングインスタンス
- セクションインスタンス
圏論的な解釈をします。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{ \mathbf{#1}}
\newcommand{\mrm}[1]{ \mathrm{#1}}
\newcommand{\In}{ \text{ in }}
`$
一般インスタンスは次の対応で説明できます。
| 型理論 | 圏論 |
|---|---|
| 型宇宙 | 圏の対象類 |
| 型 | 圏の対象 |
| 一般インスタンス | 圏の射 |
型理論のモデルとなる型理論的圏の射を一般インスタンス〈general instance〉と呼びます。
圏 $`\cat{C}`$ と特定された対象 $`I \in |\cat{C}|`$ の組 $`(\cat{C}, I)`$ を考えます。この構造を付点圏〈pointed category〉と呼びたいところですが、pointed category には別な意味があるので、特定された対象付きの圏〈category with distinguished object〉とします。特定された対象付き圏の例は：
- $`(\mbf{Set}, \mbf{1})`$ ： 集合圏と特定された単元集合
- $`(\mbf{Vect}_{\mbf{R}}, \mbf{R})`$ ： 実数体上のベクトル空間の圏とベクトル空間とみなした実数体
特定された対象付き圏 $`(\cat{C}, I)`$ において、次の形の射をポインティングインスタンス〈pointing instance〉と呼ぶことにします。
$`\quad x: I \to X \In \cat{C}`$
圏 $`\cat{C}`$ と射の集合 $`\mathscr{D}\subseteq \mrm{Mor}(\cat{C})`$ の組 $`(\cat{C}, \mathscr{D})`$ を考えます。$`\mathscr{D}`$ は、「拡張包括構造のもうひとつの定式化」で述べたディスプレイ射の集合を想定してますが、今はテキトーな集合だと思ってもいいです。
次の形の射 $`x`$ をセクションインスタンス〈section instance〉と呼ぶことにします。
$`\text{For }(p : Y \to X) \in \mathscr{D}\\
\quad x: X \to Y \In \cat{C}\\
\text{where } x;p = \mrm{id}_X
`$
「インスタンス」の使い方は人により場面により様々ですが、圏論的に解釈すれば、だいたいは、一般インスタンス、ポインティングインスタンス、セクションインスタンスのどれかだと解釈できるでしょう。例外として、ファミリー付き圏〈category with families〉による定式化などでは、インスタンスは圏のなかには存在しない（圏の外に在る）と考える場合もあります。その場合でも、圏の外にある別な圏の射がインスタンスだと考えることはできます。
