最近の型理論： 拡張包括構造を持ったインデックス付き圏

前回の記事「最近の型理論： 具体的・構文的なコンテキスト」にて：

コンテキストの水増し規則をキチンと定式化しようとすると意外と難しかったりします。

このあたりを説明するには、構文論だけではなくて意味論も紹介したほうがよさそうなので、次の機会とします。

というわけで、型理論の意味論の話をします。（[追記]意味論とは言っても、ほんとのセマンティクスと言うよりは、形式体系の構文圏〈syntactic category〉を構成する話なので、広義の構文論内部の狭義の意味論という感じです。[/追記]）

構文論／構文システムとして定義された型理論に対する圏論的意味論〈categorical semantics〉として、ファミリー付き圏〈CwF | category with families〉を使う方法が有名です。他に、局所デカルト閉圏〈LCCC | locally cartesian closed category〉を使うこともあります。

ファミリー付き圏と局所デカルト閉圏に共通する構造を、インデックス付き圏として定式化できます。ファミリー付き圏は拡張包括構造〈extension-comprehension structure〉を持ちますから、インデックス付き圏に対しても拡張包括構造を考えることにします。$`\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\hyp}{\text{－}}
\newcommand{\In}{\text{ in }}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\Fin}{\diamondsuit}
\newcommand{\hto}{\rightharpoonup}
`$

内容：

シリーズ・ハブ記事：

• 最近の型理論： 宇宙と世界、そして銀河

インデックス付き圏

サイズの問題〈size issue〉を避けたいので、小さい圏で考えます。$`\cat{C}`$ は小さい圏とします。つまり、$`\cat{C} \in |{\bf Cat}|`$ 。小さい圏の圏 $`{\bf Cat}`$ は2-圏ですが、2-射〈自然変換〉を捨てて1-圏と考えたものは $`\dimU{\bf Cat}{1}`$ とします。この書き方（次元調整）については「圏の次元調整」を見てください。

$`\cat{C}`$ から $`\dimU{\bf Cat}{1}`$ への反変関手を、$`\cat{C}`$ 上のインデックス付き圏〈indexed category〉と呼びます*1。$`\cat{P}`$ が $`\cat{C}`$ 上のインデックス付き圏であることは次のように書けます。

$`\quad \cat{P}: \cat{C}^\op \to \dimU{\bf Cat}{1} \In {\bf CAT}`$

あるいは、

$`\quad \cat{P} \in {\bf CAT}(\cat{C}^\op, \dimU{\bf Cat}{1} )`$

大きいかも知れない圏の圏 $`{\bf CAT}`$ は2-圏なので、$`{\bf CAT}(\hyp, \hyp)`$ はホム圏〈関手圏〉になります。つまり、$`\cat{C}`$ 上のインデックス付き圏の全体は（自然変換を射として）圏になります。

インデックス付き圏については、このブログ内で相当数の記事を書いています。

• 「インデックス付き圏」のブログ内検索結果

2010年の4日間内で書いた3つの記事が入門的です。

• インデックス付き圏のインデックス付き圏
• インデックス付き圏の3つの例
• インデックス付き圏のグロタンディーク構成

$`\cat{P}`$ は関手ですが、引数渡しはブラケットを使って $`\cat{P}[X], \cat{P}[f]`$ のように書くことにします。「インデックス・アクセスはブラケットで書く」という習慣からです。次の用語を使います。

• 関手 $`\cat{P}`$ の域である圏 $`\cat{C}`$ を、インデキシング圏〈indexing category〉またはベース圏〈base category〉と呼びます。インデックス付き圏とインデキシング圏が紛らわしいので主にベース圏を使います。
• ベース圏 $`\cat{C}`$ の対象・射をそれぞれベース対象〈base object〉、ベース射〈base morphism〉と呼びます。
• 特定の対象 $`X\in |\cat{C}|`$ に対する値である圏 $`\cat{P}[X] \in |{\bf Cat}|`$ は、$`X`$ 上の局所圏〈local category〉と呼ぶことにします。この「局所」は、局所デカルト閉圏の「局所」と同じ意味・用法（「各点ごと」）です。
• 局所圏 $`\cat{C}`$ の対象・射をそれぞれ局所対象〈local object〉、局所射〈local morphism〉と呼びます。

インデックス付き圏は、フィバー付き圏と対応するので、局所圏 $`\cat{P}[X]`$ はファイバー圏〈{fibre | fiber} category〉とも言えますが、ファイバー付き圏〈{fibred | fibered} category〉と紛らわしいので「局所圏」としました。が、局所射を“ファイバー方向の射”と言うことはあります。

[補足]
「ファイバー圏〈fibre category〉」と呼んだらファイバー付き圏〈fibred category〉と紛らわしいから「局所圏」と呼んだのですが、局所コンテキスト〈local context〉と一緒に語るときは混乱しそう。混乱は起きないにしても、「局所」の意味が「一点上の」と「狭いけど一点とは限らない」で齟齬は発生するでしょうね。

意味的に適切かつコンフリクトは起きないように呼び名を設定するのは難しい。
[/補足]

インデックス付き圏はグロタンディーク構成ができるので、グロタンディーク構成で平坦化〈flattening〉した圏を、

$`\quad \int \cat{P} = \int_{\cat{C}} \cat{P}[\hyp]`$

と書きます。グロタンディーク平坦化圏を、インデックス付き圏 $`\cat{P}`$ のトータル圏〈total category〉とも呼びます。この記事では、$`\cat{P}`$ のトータル圏を $`\cat{T}`$ と表すことにします。

• トータル圏 $`\cat{T}`$ の対象・射をそれぞれトータル対象〈total object〉、トータル射〈total morphism〉と呼びます。

ローマン体の $`\mrm{P}`$ は、インデックス付き圏 $`\cat{P}`$ から作ったファイバー付き圏〈ファイブレーション〉の射影の意味で使います。

$`\quad \mrm{P} : \cat{T} \to \cat{C} \In {\bf Cat}`$

まとめると：

• $`\cat{P}`$ ： インデックス付き圏
• $`\cat{C}`$ ： インデックス付き圏のベース圏
• $`\cat{P}[X]`$ ： インデックス付き圏の局所圏
• $`\cat{T}`$ ： インデックス付き圏のトータル圏
• $`\mrm{P}`$ ： ファイバー付き圏の射影関手

トータル対象とトータル射

インデックス付き圏 $`\cat{P}: \cat{C} \to \dimU{\bf Cat}{1}`$ のトータル圏 $`\cat{T} = \int \cat{P}`$ について調べましょう。

トータル圏 $`\cat{T}`$ の対象は、ベース圏 $`\cat{C}`$ の対象 $`X`$ と局所圏 $`\cat{P}[X]`$ の対象 $`A`$ のペア $`(X, A)`$ です。このペアは直積の要素ではありません。第一成分 $`X`$ によって、第二成分の選び方が制約されます。依存ペアと呼ぶものです。

集合のシグマ構成〈シグマ型〉（「リスト、タプル、タグ付きデータ、関数、依存関数」参照）を使うと、次のように書けます。

$`\quad |\cat{T}| = |\int \cat{P}| = \sum_{X \in |\cat{D}|} |\cat{P}[X]|`$

トータル圏の対象である依存ペア $`(X, A)`$ を $`A@X`$ とも書くことにします。そのココロは、「場所 $`X`$ に居る $`A`$」です。$`\cat{P}[X] = \cat{P}[Y]`$ で、$`A \in |\cat{P}[X]|`$ のときでも、$`X \ne Y`$ なら $`A@X`$ と $`A@Y`$ は違うトータル対象です。居場所が違うので。

次に、トータル射 $`f \in \mrm{Mor}(\cat{T})`$ を考えましょう。

$`\quad f: A@X \to B@Y \In \cat{T}`$

あるいは、

$`\quad f \in \cat{T}(A@X , B@Y )`$

このとき、トータル圏（グロタンディーク構成の平坦化圏）の定義により、

$`\quad f = (g, h)`$

という依存ペアで書けます。ここで、

$`\quad g: X \to Y \In \cat{C}\\
\quad h: A \to \cat{P}[g](B) \In \cat{P}[X]
`$

ここで出てきた関手 $`\cat{P}[g]:\cat{P}[Y] \to \cat{P}[X]`$ は、インデックス付き圏の再インデキシング関手〈reindexing functor〉と呼びます。インスティチューション理論ではリダクト関手〈reduct functor〉と言います。言いやすいという理由で、「リダクト関手」を使うことにします。リダクト関手は $`g^*`$ と略記されることがあります（もちろん、$`\cat{P}`$ は周知として）。

トータル圏に埋め込まれた局所圏 $`\cat{P}[X]`$ は、ファイブレーション射影の逆像とみなせます。

$`\quad P^{-1}(X) \cong \cat{P}[X] \In \dimU{\bf Cat}{1}`$

ファイバー〈逆像〉としての局所圏を $`\cat{T}_{@X}`$ と書くことにします。

$`\quad \cat{T}_{@X} := P^{-1}(X) \cong \cat{P}[X]\\
\quad \cat{T}_{@X} \subseteq \cat{T}
`$

これらの記法を使うと、トータル射は次のように記述できます。

$`\quad f: A@X \to B@Y \In \cat{T}\\
\quad f = (g, h)\\
\text{where }\\
\quad g : X \to Y \In \cat{C}\\
\quad h : A@X \to g^*(B@Y) \In \cat{T}_{@X}\\
\quad :\Iff h : A \to g^* B \In \cat{P}[X]
`$

トータル射は、2つの成分 $`g, h`$ に分解できますが、分解した成分の呼び名は色々あります。

• $`g`$ はベースパート、$`h`$ はファイバーパート
• $`g`$ は第一成分、$`h`$ は第二成分
• $`g`$ は第一射影、$`h`$ は第二射影

型理論の圏論的意味論（特にファミリー付き圏）の文脈では、第一射影／第二射影が使われるようです。ただし、第 i 成分（i = 1 or 2）を取り出す操作や、第 i 成分を取り出すときに使う特別な射も第 i 射影と多義的に使われています。多義性には要注意です（[追記]「型理論に出てくる第一射影と第二射影」参照[/追記]）。

トータル射 $`f`$ を $`f = (g, h)`$ と分解したとき、このペアは依存ペアなので、$`g`$ によって、第二成分として選べる $`h`$ は制約がかかります。トータル射の集合、つまりトータル圏のホムセットは次のようにシグマ型を使って書けます。

$`\quad \cat{T}(A@X, B@Y) = \sum_{g\in \cat{C}(X, Y)}\cat{P}[X](A, g^* B)`$

ベース対象の拡張

$`\cat{P}`$ は、ベース圏 $`\cat{C}`$ 上のインデックス付き圏とします。$`\cat{P}`$ のすべての局所圏は終対象を持つとします。それらの終対象は $`{\bf 1}@X`$ で表すことにします。$`{\bf 1}`$ は次のようなセクションになっています。

$`\quad {\bf 1} : X \mapsto {\bf 1}@X \: \text{ where } P({\bf 1}@X) = X\\
\quad {\bf 1} : |\cat{C}| \to \sum_{X\in |\cat{C}|} | \cat{P}[X] | \:\text{ section}`$

したがって、$`{\bf 1}`$ はパイ型の要素です。

$`\quad {\bf 1} \in \prod_{X\in |\cat{C}|} | \cat{P}[X] |`$

すべてのリダクト関手は終対象を厳密に保存すると仮定します。

$`\text{For }f:X \to Y \in \cat{C}\\
\quad f^*({\bf 1}@Y) = {\bf 1}@X
`$

また、ベース圏 $`\cat{C}`$ も終対象を持つとします。ベース圏の終対象は、局所圏の終対象とは区別して、$`\Fin`$ で表します。この記号は、「最近の型理論： 具体的・構文的なコンテキスト」における空コンテキスト $`\langle\rangle`$ に似せたものです。

このようなインデックス付き圏 $`\cat{P}`$ は、「最近の型理論： 具体的・構文的なコンテキスト」で述べた具体的・構文的な概念と次のように対応します。

ベース対象	コンテキスト
ベース終対象	空コンテキスト
局所対象	型（型項のセマンティクス）
局所終対象	ユニット型（型定数 $`\mathsf{I}`$ のセマンティクス）
局所終対象からの局所射	インスタンス（インスタンス項のセマンティクス）
トータル対象	コンテキストと型のペア（判断のセマンティクス）

具体的・構文的なコンテキストにおけるコンテキスト拡張〈context extension〉は、既存のコンテキストに、型付きの自由変数（自由変数の型宣言）を追加することでした。追加する型は、判断 $`\Gamma \vdash \alpha {\bf \text{ type-term}}`$ で正当性が保証されたものです。

コンテキスト拡張に対応する意味論的概念〈セマンティクス〉は、インデックス付き圏のベース対象の拡張〈base object extension〉です。

• 既存コンテキストに相当するものは、ベース対象 $`X \in |\cat{C}|`$
• 判断（により正当化されたペア）に相当するものは、局所対象 $`(X, A) = A@X`$
• 追加する型に相当するものは、局所対象 $`A = A@X`$
• 変数（の名前）に相当するものはない。

ベース対象 $`X`$ を、局所対象 $`A = A@X`$ で拡張した対象〈extended object〉を $`X\cdot A`$ と書きます*2。これは、$`A@X \mapsto X\cdot A`$ ともみなせるので、拡張演算 $`(\hyp \cdot \hyp)`$ は次のような写像です。

$`\quad (\hyp \cdot \hyp) : (|\cat{T}| = \sum_{X \in |\cat{C}|} |\cat{P}[X]| ) \to |\cat{C}|
`$

特定のベース対象 $`X`$ に対する拡張 $`(X \cdot \hyp)`$ は次のような写像です。

$`\quad (X \cdot \hyp) : (|\cat{T}_{@X}| = |\cat{P}[X]| ) \to |\cat{C}|`$

ベース終対象 $`\Fin`$ の $`A \in |\cat{P}[\Fin]|`$ による拡張は次のように書きます。

$`\quad \Fin \cdot A = \langle A\rangle \;\in |\cat{C}|`$

ベース対象 $`\langle A\rangle`$ を $`B \in |\cat{P}[\langle A\rangle]|`$ により拡張した対象は次のように書きます。

$`\quad \langle A\rangle \cdot B = \langle A, B\rangle \;\in |\cat{C}|`$

同様に続けると、局所対象を並べたリストの形になります。

$`\quad \langle A_1, A_2, \cdots ,A_n\rangle \;\in |\cat{C}|`$

局所対象のベースパートも書き込むと、入れ子の構造になります。

$`\quad \langle A_1@\Fin, A_2@\langle A_1\rangle, \cdots ,A_n@\langle A_1, A_2, \cdots, A_{n - 1}\rangle\rangle \;\in |\cat{C}|`$

この入れ子構造を持ったリストが、変数（の名前）を取り去ったコンテキストの意味論的対応物になります。名前がなくなっているので、リネームによる同値性〈アルファ同値〉を考える必要がありません。名付けとリネームがなくなるだけでも随分と取り扱いが楽になります。

インスタンス射、非局所インスタンス射、ハープーン射

前節同様、$`\cat{P}`$ は、ベース終対象付き・局所終対象付きなインデックス付き圏だとします。これは、ベース圏が終対象付き圏〈category with {terminal | final} object〉で、すべての局所圏が終対象付き圏で、すべてのリダクト関手が終対象を（厳密に）保存することです。

インデックス付き圏において、ベース射はいわば横〈水平〉方向な射で、局所射は縦〈鉛直 | 垂直〉方向の射です。トータル射は横と縦を組み合わせたペアになります。型理論において特に重要な射は、局所終対象から出る局所射 -- インスタンス射〈instance morphism〉です。

一般に、圏 $`\cat{D}`$ が終対象 $`{\bf 1}`$ を持つとき、圏の対象を型とみて、型 $`A`$ のインスタンス射の集合を次のように書きます。

$`\text{For } A \in |\cat{D}|\\
\quad \mrm{Inst}_{\cat{D}}(A) := \cat{D}({\bf 1}, A)`$

インデックス付き圏 $`\cat{P}`$ （ベース圏は $`\cat{C}`$）の場合は、次のようになります。

$`\text{For } X \in |\cat{C}|, A \in \cat{P}[X]\\
\quad \mrm{Inst}_{\cat{P}}(X, A) := \cat{P}[X]({\bf 1}, A)`$

インスタンス射は定義より局所射（縦方向の射）ですが、域〈domain〉が局所終対象であるトータル射もインスタンス射とみなします。ただし、こちらは局所射とは限らないので非局所インスタンス射〈non-local instance morphism〉と呼ぶことにします。

$`\text{For } W, X \in |\cat{C}|, A \in \cat{P}[X]\\
\quad \mrm{Inst}_{\cat{P}}(W, A@X) := \cat{T}({\bf 1}@W, A@X)
= \sum_{g\in \cat{C}(W, X)} \cat{P}[W]({\bf 1}, g^* A)`$

非局所インスタンス射はトータル射なので、ベース射 $`g:W \to X \In \cat{C}`$ とインスタンス射〈局所インスタンス射〉 $`h : {\bf 1} \to g^* A \in \cat{P}[W]`$ のペアで表現されます。局所インスタンス射は縦方向ですが、非局所インスタンス射は斜め方向も許します。

非局所インスタンス射 $`f: {\bf 1}@W \to A@X \In \cat{T}`$ を次の形にも書きます。

$`\quad f: W \hto A@X \In \cat{T}`$

この形に書いたときは、$`\cat{T}`$ の（または $`\cat{P}`$ の）ハープーン射と呼びます。矢印記号にハープーン（銛矢印、LaTeXでは \rightharpoonup）を使っているからです。

ハープーン射と非局所インスタンス射は、実体としては同じものです。が、ハープーン射と呼ぶ場合は、ベース対象 $`W`$ を域として、$`X`$ 上の局所対象 $`A = A@X`$ を余域とする射のように扱います。

ベース射とハープーン射を結合することができて、結合の結果はハープーン射です。なぜなら； $`k:V \to W \In \cat{C}`$ がベース射のとき、ペア $`(k, \mrm{id}_{{\bf 1}@V})`$ はトータル射で、トータル射としてハープーン射と結合できるからです。この結合方法で、ベース射と局所インスタンス射も結合できます（局所インスタンス射は特殊なハープーン射）。

ハープーン射（非局所インスタンス射と同じもの）$`f`$ は、トータル射として $`f = (g, h)`$ のように分解できます。ベースパートを明示する場合、あるいはベース射を固定して考える場合は次のように書きます。

$`\quad f: W \underset{g}{\hto} A@X \In \cat{T}\\
\Iff (g, h): W \underset{g}{\hto} A@X \In \cat{T}\:\text{ 冗長な書き方}\\
\Iff h: W \underset{g}{\hto} A@X \In \cat{T}\:\text{ 簡潔に略記}
`$

ハープーン射における記号の乱用は $`h = (g, h)`$ の形にします。つまり、ベースパートは暗黙に仮定して、ファイバーパートだけ明示的に書くという流儀です。

型理論の圏論的意味論の文脈では、ハープーン射は非常に重要です。なぜなら、ハープーン射は、型コンテキストを前提としたインスタンス項の型判断に対応するからです。また、次節で述べる拡張包括構造のもとでは、ベース射はハープーン射を積み重ねて構成されます*3。

拡張包括構造

型理論の意味論として使われるインデックス付き圏は、ベース圏とトータル圏が密接に関連しています。ベース対象拡張により、トータル対象にベース対象が対応しているだけでなく、拡張された対象〈extended object〉を含むベース圏のホムセットとトータル圏のホムセットも同型で関係付けられます。ベース対象拡張演算に伴う射の関係付けの構造を拡張包括構造〈extension comprehension structure〉と呼びましょう。ファミリー付き圏では、コンテキスト拡張〈context extension〉／コンテキスト包括〈context comprehension〉と呼んでいます。

拡張包括構造は、ベース対象 $`W, X`$ と局所対象 $`A = A@X`$ に対して、次のホムセット同型を系統的に与えます。

$`\quad \cat{C}(W, X\cdot A) \cong \cat{T}({\bf 1}@W, A@X) = \sum_{g \in \cat{C}(W, X)}\cat{P}[W]({\bf 1}, g^* A) \In {\bf Set}`$

任意のベース対象 $`W`$ から拡張された対象 $`X\cdot A`$ へのベース射 $`f`$ は、とあるトータル射 $`(g, h)`$ と1：1対応します。この同型を「系統的に与える」メカニズムが拡張包括構造です。

ヒントになる（一番簡単な）ケースは、デカルト圏の直積の場合の次の同型です。

$`\quad \cat{C}(W, X\times A)\cong \cat{C}(W, X) \times \cat{C}(W, A) \In {\bf Set}`$

デカルト圏の直積の場合は、右辺がホムセットの単純な直積ですが、拡張〈extension〉の場合の右辺はシグマ型で与えられます。第一成分を取り出す方法は、デカルト圏の場合とソックリです。第二成分はちょっと複雑です。

拡張包括構造においては、ベース対象拡張 $`X\cdot A`$ に対して、第一射影（と呼ばれる特定のベース射）が決まります。それは次の形です。

$`\quad p^{X, A} :X\cdot A \to X \In \cat{C}\\
\Iff p^{X, A} \in \cat{C}(X\cdot A, X)
`$

$`f:W \to X\cdot A \In \cat{C}`$ の第一成分（$`X`$-成分）$`g`$ を取り出すには、$`f`$ に第一射影を後結合〈post-compose〉すればOKです。デカルト圏のときと同じですね。

$`\text{For }f \in \cat{C}(W, X\cdot A)\\
\quad g := f; p^{X, A} \in \cat{C}(W, X)`$

第二成分（$`A`$-成分）を取り出すために使う第二射影（と呼ばれる特定の非局所インスタンス射）を、ハープーン射として書けば次の形です。

$`\quad q^{X, A} : X\cdot A \underset{p^{X, A}}{\hto} A@X \In \cat{T}\\
\Iff (p^{X, A}, q^{X, A}) : {\bf 1}@(X \cdot A) \to A@X \In \cat{T}\\
\Iff q^{X, A} \in \cat{T}_{@(X\cdot A)}({\bf 1}@(X \cdot A), (p^{X, A})^*(A@X) )\\
\Iff q^{X, A} \in \cat{P}[X\cdot A]({\bf 1}, (p^{X, A})^* A)
`$

$`f:W \to X\cdot A \In \cat{C}`$ の第二成分（$`A`$-成分）$`h`$ を取り出すには、$`f`$ に第二射影を後結合します。

$`\text{For }f \in \cat{C}(W, X\cdot A)\\
\quad h := f; q^{X, A} \in \cat{T}_{@W}({\bf 1}@W, X)`$

ここでの結合 '$`;`$' は、ベース射とハープーン射の結合の意味です。

“ハープーン射”と“ベース射とハープーン射の結合”という概念を使うと、成分の取り出し方を一律に表現できます。

• ベース射 $`f`$ の第一成分 $`g`$ は、$`g := f; p^{X, A}`$ として取り出す。
• ベース射 $`f`$ の第二成分 $`h`$ は、$`h := f; q^{X, A}`$ として取り出す。

ベース射 $`f`$ から作られたペア $`(g, h)`$ はトータル射となります。逆向きに、トータル射からベース射を構成する演算は記号 $`\langle \hyp \,\&\, \hyp\rangle`$ で表すことにします。

$`\quad (g, h) \mapsto \langle g \,\&\, h \rangle := f`$

としてベース射 $`f`$ を再現できます。$`\langle \hyp \,\&\, \hyp\rangle`$ を依存ペアリング〈dependent pairing〉と呼ぶことにします。

以上のメカニズムにより、本節冒頭の同型が与えられます。

$`\quad \cat{C}(W, X\cdot A) \cong \cat{T}({\bf 1}@W, A@X) = \sum_{g \in \cat{C}(W, X)}\cat{P}[W]({\bf 1}, g^* A) \In {\bf Set}`$

まとめ

拡張包括構造を持ったインデックス付き圏 $`\cat{P}`$ があると、“密接な関係を持ったトータル圏とベース圏”からなるファイバー付き圏 $`P:\cat{T}\to \cat{C}`$ を作れます。密接な関係とは次のようなものです。

• ベース圏の対象は、拡張演算 $`(\hyp \cdot \hyp)`$ によりトータル圏の対象（ベース対象・局所対象の依存ペア）から構成できる。
• ベース圏の射は、依存ペアリング $`\langle \hyp \,\&\, \hyp\rangle`$ によりトータル圏の射（ベース射・局所射の依存ペア）から構成できる。
• ベース圏は、終対象を使った“持ち上げ”により、トータル圏のなかに埋め込める。この埋め込みはファイバー付き圏のセクションになる。

拡張包括構造は、デカルト構造の一般化とみなすことができます。

デカルト構造	拡張包括構造
デカルト積	ベース対象拡張
デカルト積の第一射影	ベース対象拡張の第一射影
デカルト積の第二射影	ベース対象拡張の第二射影
射のデカルト・ペアリング	ベース射とハープーン射の依存ペアリング

*1:この定義は、厳密インデックス付き圏〈strict indexed category〉を定義します。弱いバージョンの定義もありますが、話がややこしくなります。

*2:「最近の型理論： 拡張包括構造を持ったインデックス付き圏」においては、記号 '$`\cdot`$' は具体的なリスト演算でした。ここでの '$`\cdot`$' は抽象的な演算を表す記号です。

*3:構文論において、一般的な代入〈substitution〉操作が単純代入の積み重ねとして書けることに対応します。