包括コンテキスタッドに向けて - 檜山正幸のキマイラ飼育記 (はてなBlog)

包括圏とコンテキスタッドの組み合わせは、型理論やインスティチューション理論に向いているようです（「型理論とコンテキスタッド：コンテキストフル射」参照）。この記事では、包括コンテキスタッド（包括圏とコンテキスタッドの組み合わせ）を定義し利用するために必要な諸々の準備的事項をバラバラと記します。コンテキスタッドのための用語集〈グロッサリー〉といった趣です。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mbb}[1]{ \mathbb{#1} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
\newcommand{\ctxpair}[2]{ \begin{pmatrix}#1 \\ #2\end{pmatrix} }
\newcommand{\fibot}{\twoheadleftarrow}
\newcommand{\fibto}{\twoheadrightarrow}
\newcommand{\cofibto}{ \rightarrowtail }
\newcommand{\cofibot}{ \leftarrowtail }
\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
`$

内容：

ファイブレーション
ファミリー〈インデックス付き圏〉
グロタンディーク構成と逆グロタンディーク構成
ファイブレーション的プルバック四角形
デカルト持ち上げと亀裂子／分裂子
反ファイブレーション
局所ホニャララ・ファイブレーション
中置演算子記号の使い方
セクションとレトラクション
トータル射の結合公式と図示
おわりに

補足：

グロタンディーク対応

追記：

終対象の保存

ハブ記事：

コンテキスタッド、包括圏、ハイパードクトリン

ファイブレーション

ファイブレーションに関する過去記事達（古い順）を挙げておきます。

ファイブレーション〈fibration | グロタンディーク・ファイブレーション | ファイバー付き圏 | 圏のバンドル〉を次のように書きます。

$`\quad \pi : \cat{D} \to \cat{C} \In \mbf{CAT}`$

構成素の呼び名は：

$`\cat{C}`$ ： ベース圏〈base category〉
$`\cat{D}`$ ： トータル圏〈total category〉
$`\pi`$ ：射影〈projection〉

記号の乱用で次のようにも書きます。

$`\quad \cat{D} = (\cat{C}, \cat{D}, \pi_{\cat{D}})`$

もし、ファイブレーション自体とそのトータル圏を区別したいなら：

$`\quad \cat{D} = (\cat{C}, \o{\cat{D}}, \pi_{\cat{D}})`$

実際のところは $`\cat{D} = \pi_{\cat{D}}`$ です。なぜなら、上の書き方は関手 $`F`$ を次の形に書いていることになるからです。

$`\quad F = (\mrm{cod}(F), \mrm{dom}(F), F)`$

関手 $`\pi`$ に関して言うなら：

$`\mrm{cod}(\pi) = \cat{C}`$
$`\mrm{dom}(\pi) = \o{\cat{D}}`$
$`\pi = \cat{D}`$

すべてのファイブレーション達の集合は、$`\mrm{Mor}(\mbf{CAT})`$ の部分集合で、圏 $`\cat{C}`$ 上のファイブレーション達の集合は、$`\mrm{Obj}(\mbf{CAT}/\cat{C})`$ の部分集合です。ここで、$`\mbf{CAT}/\cat{C}`$ はオーバー圏〈スライス圏〉です。

ベース圏の対象 $`X\in|\cat{C}|`$ に対して、$`\pi^{-1}(X)`$ はトータル圏 $`\cat{D}`$ の部分圏です。この部分圏を $`\cat{D}_X`$ または $`\cat{D}_{@X}`$ と書きます。圏 $`\cat{D}_{@X}`$ を、$`X`$ 上のファイバー〈fiber〉または局所圏〈local category〉と呼びます。局所圏〈ファイバー〉は空圏〈empty category〉かも知れません。

ベース圏／トータル圏／局所圏の対象・射をそれぞれ、ベース対象・射／トータル対象・射／局所対象・射と呼びます*1。局所対象・射はトータル対象・射です。トータル対象・射は、どれかの局所圏の局所対象・射です。つまり、局所なのかトータルなのかは、見方の問題で、対象・射自体を局所かトータルかに分類できるわけではありません*2。

ファミリー〈インデックス付き圏〉

圏のファミリー〈インデックス付き圏〉に関する過去記事達（古い順）を挙げておきます。

圏のファミリー〈family of categories | インデックス付き圏 | 圏のインデキシング〉を次のように書きます。

$`\quad \cat{F} : \cat{C}^\op \to \mbf{CAT} \In 2\mbb{CAT}`$

$`\cat{C}`$ を、$`\cat{F}`$ のベース圏〈base category〉またはインデキシング圏〈indexing category〉と呼びます。

冗長表現（記号の乱用ではない）で次のようにも書きます。

$`\quad \cat{F} = (\cat{C}, \cat{F})`$

上の書き方は反変関手 $`F`$ を次の形に書いていることになります。

$`\quad F = (\mrm{dom}(F)^\op, F)`$

ファイブレーション〈ファイバー付き圏〉では関手の余域をベース圏と呼び、ファミリー〈インデックス付き圏〉では関手の域をベース圏と呼んでいるので注意してください。

グロタンディーク構成と逆グロタンディーク構成

圏のファミリー〈インデックス付き圏〉 $`\cat{F}:\cat{C}^\op \to \mbf{CAT}`$ に対して、そのグロタンディーク構成を次のように書きます。

$`\quad \int\cat{F} = \int_{\cat{C}}\cat{F} = \int(\cat{C}\mid \cat{F})`$

グロタンディーク構成の結果を単なる圏と見るかファイブレーションと見るかは文脈依存（曖昧）です。構成の結果がファイブレーションであるとして、それを記号の乱用で書けば次のようです。記号の乱用が、曖昧さに対応しています。

$`\quad \int\cat{F} = (\cat{C}, \int\cat{F}, \pi_{\int \cat{F}})`$

「ファイブレーション」の節で注意したように、この書き方では：

$`\mrm{cod}(\pi_{\int\cat{F}}) = \cat{C}`$
$`\mrm{dom}(\pi_{\int\cat{F}}) = \int\cat{F}`$
$`\pi_{\int\cat{F} } = \int\cat{F}`$

$`\pi_{\int\cat{F} }`$ は通常 $`\pi_{\cat{F} }`$ と略記します。記号の乱用、冗長表現、省略が重なると、書かれたテキストと実際のところ（事実）が乖離します。乖離を埋める作業が常に必要です。

圏 $`\cat{C}`$ 上のファイブレーション $`\cat{D}`$ （記号の乱用なので、ほんとは $`\pi = \cat{D} :\o{\cat{D}}\to \cat{C}`$）の局所圏〈ファイバー〉 $`\cat{D}_{@X}`$ の下付きを大きく書いて $`\cat{D}@X`$ でもいいとします。さらに、$`\cat{D}@(X)`$ とも書いて、$`\cat{D}@`$ は次のような関手とみなします。

$`\quad \cat{D}@ : \cat{C}^\op \to \mbf{CAT} \In 2\mathbb{CAT}`$

つまり、$`\cat{D}\mapsto \cat{D}@`$ を逆グロタンディーク構成（「グロタンディーク構成・逆構成と同値対応」参照）だとします。$`\cat{D}@`$ は逆グロタンディーク構成のアットマーク記法〈atmark notation〉です。

圏 $`\cat{C}`$ 上のファイブレーション〈ファイバー付き圏〉達の圏を $`\mbf{FibCAT}[\cat{C}]`$ 、圏 $`\cat{C}`$ 上のファミリー〈インデックス付き圏〉達の圏を $`\mbf{IndCAT}[\cat{C}]`$ とすると、次のような圏同値があります。

$`\quad \xymatrix@C+1pc{
{\mbf{FibCAT}[\cat{C}]} \ar@/^1pc/[r]^{(\hyp)@}
&{\mbf{IndCAT}[\cat{C}]} \ar@/^1pc/[l]^{\int (\hyp)}
}\\
\quad \text{equivalence }\In \mathbb{CAT}
`$

アットマークの後置と積分記号の前置がほぼ逆の操作です。

[補足]
グロタンディーク構成と逆グロタンディーク構成による、ファイブレーション-ファミリーの対応はグロタンディーク対応〈Grothendieck correspondence〉と呼べばよさそうです。実際、そう呼んでいる例もあるのですが意外と少数です。

"Grothendieck correspondence" と検索すると、グロタンディークとセールの文通〈往復書簡〉の記録がヒットします。

https://webusers.imj-prg.fr/~leila.schneps/grothendieckcircle/Letters/GS.pdf

グロタンディークは色々な人と手紙のやり取りをしたので、"correspondence" が「文通」を連想させてしまうのかも知れません。それで、Grothendieck correspondence が用語として若干使いにくいって事情はありそうです。
[/補足]

ファイブレーション的プルバック四角形

関手のデカルト射については以下の記事で述べています。

関手のデカルト射とファイバー付き圏

上記の過去記事内では、圏のなかではなくて関手のなかに描く図式〈関手ターゲットの図式〉についても触れています。$`\pi : \cat{D} \to \cat{C}`$ をファイブレーションの射影（実はファイブレーションそのもの）だとして、関手 $`\pi`$ のなかに次の図式を描けます。

$`\quad \xymatrix{
\cdot \ar[r]^g \ar@{|->}[d]_\pi
&{B} \ar@{|->}[d]^\pi
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi: \cat{D}\to\cat{C}
`$

上段はトータル圏 $`\cat{D}`$ 、下段はベース圏 $`\cat{C}`$ を表します。この図式が、$`\pi`$ のデカルト射 $`g`$ を定義する図式（「関手のデカルト射とファイバー付き圏」参照）であるとき、プルバック四角形と似ているので、ファイブレーション的プルバック四角形〈fibrational pullback square〉、またはファイブレーション的デカルト四角形〈fibrational Cartesian square〉と呼ぶことにします。ファイブレーション的プルバック四角形は、内部に $`\text{f.p.b.}`$ と書いて識別することにします。

上の図をファイブレーション的プルバック四角形だとして、デカルト射 $`g`$ は $`f`$ のデカルト持ち上げ〈Cartesian lift〉です。デカルト持ち上げを次のように書きます。

$`\quad g = f^{\Uparrow B}`$

デカルト持ち上げ $`f^{\Uparrow B}`$ の余域（トータル圏の対象）を $`f^* B, f^\# B, f^\diamond B`$ などで書きます。

これらの約束に従い、もう一度ファイブレーション的プルバック四角形を描くと：

$`\quad \xymatrix{
{f^* B} \ar[r]^{f^{\Uparrow B}} \ar@{|->}[d]_\pi
\ar@{}[dr]|{\text{f.p.b.}}
&{B} \ar@{|->}[d]^\pi
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi: \cat{D}\to\cat{C}
`$

よく出てくるけど、ややこしいのは、$`\cat{D} = \mrm{Arr}(\cat{C})`$ で、ファイブレーションの射影がコドメイン関手 $`\mrm{Cod}:\mrm{Arr}(\cat{C})\to\cat{C}`$ のときです。ファイブレーション的プルバック四角形は次のように描けます。

$`\quad \xymatrix{
{f^* u} \ar[r]^{f^{\Uparrow u}} \ar@{|->}[d]_{\mrm{Cod}}
\ar@{}[dr]|{\text{f.p.b.}}
&{u} \ar@{|->}[d]^{\mrm{Cod}}
\\
X \ar[r]_f
&Y
}\\
\quad \In \mrm{Cod} : \mrm{Arr}(\cat{C})\to\cat{C}
`$

上段の $`f^{\Uparrow u}`$ は $`\mrm{Arr}(\cat{C})`$ の射、つまり $`\cat{C}`$ 内の可換四角形です。特に $`\mrm{Cod}`$ のデカルト射になっているので、$`\cat{C}`$ 内のプルバック四角形です。プルバック四角形を $`\cat{C}`$ 内に展開して（普通に）描けば次のようです。

$`\quad \xymatrix{
\cdot \ar[r] \ar[d]_{{f^* u}}
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]^{u}
\\
X \ar[r]_f
&Y
}\\
\quad \In \cat{C}
`$

ファイブレーション的プルバック四角形とプルバック四角形は強く関係していますが、描かれている場所が違います。例えば、プルバック四角形の上段の矢印は $`\mrm{Dom}(f^{\Uparrow u})`$ です。ファイブレーション的プルバック四角形とプルバック四角形の関係と違いをよーく確認しましょう。

デカルト持ち上げと亀裂子／分裂子

前節で導入した記法 $`f^{\Uparrow B}`$ は、$`\hyp^{\Uparrow \hyp}`$ という二項演算子の値（適用結果）だと言えます。この二項演算子の域は次のような集合です。

$`\quad \{(f, B)\in \mrm{Mor}(\cat{C})\times \mrm{Obj}(\cat{D}) \mid \mrm{cod}(f) = \pi(B) \}`$

$`f^{\Uparrow B}`$ はデカルト持ち上げですが、デカルト持ち上げの一意性は保証されないので、幾つかある（かも知れない）デカルト持ち上げからひとつを選んで対応させる写像が $`\hyp^{\Uparrow \hyp}`$ です。

デカルト持ち上げを選んで対応させる写像を（ファイブレーションの）亀裂子〈cleavage〉と呼びます（「ファイブレーションの亀裂と分裂」「圏のファイブレーション」参照）。亀裂子がないと不便すぎるので、ファイブレーションには亀裂子が存在すると仮定します。特定の亀裂子を固定したファイブレーションを亀裂子付きファイブレーション〈cloven fibration | fibration with cleavage〉と呼びます。

単にファイブレーションといった場合でも亀裂子が固定されていることがあるので、「ファイブレーション」と「亀裂子付きファイブレーション」の違いは曖昧にされることがあります。「亀裂子はあえて固定はしないが、必要ならいつでも亀裂子を選んで固定する」という態度が多いようです。

いずれにしても、二項演算子記号 $`\hyp^{\Uparrow \hyp}`$ は、ファイブレーションの亀裂子を表します。亀裂子が次の等式を満たすとき分裂子〈splitting〉と呼びます。

$`\text{For }f:X \to Y, g:Y \to Z \In \cat{C}\\
\text{For }C \in |\cat{D}_{@Z}|\\
\quad (f; g)^{\Uparrow C}
= f^{\Uparrow (g^* C)}; g^{\Uparrow C}\\
\quad {\id_Z}^{\Uparrow C} = \id_{C}
`$

最初の等式は、ファイブレーション的プルバック四角形を使って次のように描けます。

$`\quad \xymatrix{
{f^* (g^* C)} \ar[r]^-{f^{(\Uparrow g^* C)}} \ar@{|->}[d]_{\pi}
\ar@{}[dr]|{\text{f.p.b.}}
&{g^* C} \ar[r]^{g^{\Uparrow C}} \ar@{|->}[d]|{\pi}
\ar@{}[dr]|{\text{f.p.b.}}
&C \ar@{|->}[d]^{\pi}
\\
X \ar[r]_{f}
&Y \ar[r]_{g}
&Z
}\\
\quad \In \pi : \cat{D}\to\cat{C}
`$

特定の分裂子を固定したファイブレーションを分裂子付きファイブレーション〈fibration with splitting〉と呼びます。分裂子が存在するファイブレーションは分裂可能ファイブレーション〈splittable fibration〉です。分裂ファイブレーション〈split fibration〉が、分裂可能ファイブレーションのことか分裂子付きファイブレーションなのかは曖昧です。が、曖昧でもあまり困ることはないでしょう。

反ファイブレーション

反ファイブレーション〈opfibration〉または余ファイブレーション〈cofibration〉は、ファイブレーションの双対概念です。

関手のデカルト射の代わりに、関手の反デカルト射〈opCartesian morphism〉を考える。
ファイブレーション的プルバック四角形の代わりに、反ファイブレーション的プッシュアウト四角形〈opfibrational pushout square〉を考える。
ベース圏の射〈ベース射〉 $`f:X\to Y`$ と $`X`$ 上の局所圏〈ファイバー〉の対象 $`A`$ に対して、反デカルト持ち上げ〈opCartesian lift〉 $`{^{\Uparrow A}f}`$ が（up-to-isoで）決まる。
インデックス付き圏の代わりに、余インデックス付き圏〈圏の余ファミリー〉を考える。
圏 $`\cat{C}`$ をベース圏とする反ファイブレーション達の圏と、圏 $`\cat{C}`$ をベース圏とする余インデックス付き圏達の圏のあいだには、グロタンディーク構成／逆グロタンディーク構成による圏同値がある。

接頭辞「反〈op〉」と「余〈co〉」は交換可能で、これといった違いや運用ルールはないようです。「反」「余」の選択は、好みと習慣に従えばいいでしょう。

局所ホニャララ・ファイブレーション

$`\pi:\cat{D}\to \cat{C}`$ はファイブレーションとします。どの $`X\in |\cat{C}|`$ に対しても、局所圏 $`\cat{D}_{@X}`$ がホニャララな構造を持つとき、ファイブレーションは局所ホニャララ〈locally blah-blah-blah〉であるといいます。例えば、$`\cat{D}_{@X}`$ がモノイド圏の構造を持つなら局所モノイド・ファイブレーション〈locally monoidal fibration〉です*3。

局所的（ベース対象ごとの）構造について述べるときは、ファイブレーション $`\cat{D}`$ に対応するファミリー〈インデックス付き圏〉$`\cat{D}@`$ を考えたほうが分かりやすいでしょう。$`\cat{D}@`$ が値を取る圏がホニャララであれば、局所ホニャララです。例えば、局所モノイド・ファイブレーションに対応するファミリーは次の形です。

$`\quad \cat{D}@ : \cat{C}^\op \to \mbf{MonCAT} \In 2\mbb{CAT}`$

ここで、$`\mbf{MonCAT}`$ は、モノイド圏／モノイド関手／モノイド自然変換からなる2-圏です。$`\cat{C}^\op`$ は1-圏ですが、規準的に2-圏とみなすことが出来ます（「変換手n-圏のブラケット記法」参照）。

圏 $`\cat{C}`$ が局所デカルト閉圏〈locally Cartesian closed category〉であるとは、$`X\mapsto \cat{C}/X`$ から定義される関手が局所デカルト閉ファイブレーションになることです。

$`\quad \cat{C}/(\hyp) : \cat{C}^\op \to \mbf{CartClosedCAT} \In 2\mbb{CAT}`$

もっと簡単な事例として、局所的に終対象を持つファイブレーションは、特定された終対象を持つ圏達／終対象を保存する関手達／自然変換達からなる2-圏を $`\mbf{CATwTermi}`$ （category with terminal object）として、次の形です。

$`\quad \cat{F} : \cat{C}^\op \to \mbf{CATwTermi} \In 2\mbb{CAT}`$

[追記]
特定された終対象を持つ圏を対象とする圏や2-圏において、射は終対象を保存するように決めるのがなんとなく自然に思えます。上の定義はそのようにしています。しかし、実例を見ると、終対象を保存しない関手も考えたほうが面白いときがあるようです。

つまり、対象が特定された終対象を持つ圏であっても、射は無条件の関手、2-射は自然変換という2-圏を考えるケースもある、ということです。一般的に、対象が構造付き圏であっても、その構造を必ずしも保存しない関手を射にすることは、ときに必要です。
[/追記]

さらに簡単な事例は、局所離散ファイブレーションです。これは単に離散ファイブレーション〈discrete fibration〉と呼ばれています。

中置演算子記号の使い方

包括圏やコンテキスタッドでは、次のような自己スパン〈endo-span〉が出てきます。

$`\quad \cat{C} \overset{\pi}{\leftarrow} \cat{D} \overset{\alpha}{\to}\cat{C}
\In \mbf{CAT}
`$

左脚 $`\pi`$ はファイブレーションです（反ファイブレーションのときもあります）。右脚 $`\alpha`$ は事例ごとに固有な呼び名があるでしょうが、一般的には作用〈action〉と呼びます。

作用は、二項演算子記号、例えば $`\odot`$ で書かれることがしばしばあります。二項演算子記号を、通常の関手として扱うときは（Haskellなどと同じ流儀で）丸括弧で囲むことにします。

$`\quad (\odot) : \cat{D} \to \cat{C}\In \mbf{CAT}`$

ファイブレーションのトータル圏 $`\cat{D}`$ の対象は、依存ペアにより $`(X, A)`$ と書きます。カプチ／マイヤースに倣って縦ベクトル記法 $`\ctxpair{A}{X}`$ も使います（「型理論とコンテキスタッド：コンテキストフル射」参照）。

$`\quad A = (X, A) = \ctxpair{A}{X}\\
\text{Where}\\
\quad X \in |\cat{C}|\\
\quad A \in |\cat{D}_{@X}|
`$

ここで、$`A = (X, A)`$ は記号の乱用ではないので注意してください。依存ペア $`(X, A)`$ は次の状況を表現しています。

$`\quad \xymatrix{
A \ar@{|->}[d]^\pi
\\
X
}\\
\quad \In \pi : \cat{D} \to \cat{C}
`$

依存ペアと中置演算子記号の関係は次のようです。

$`\quad (\odot)(A) = (\odot)(\ctxpair{A}{X}) = (\odot) A = (\odot)\ctxpair{A}{X} = X\odot A`$

ファイブレーションのトータル圏の射 $`F`$ があるとします。

$`\quad F : \ctxpair{A}{X} \to \ctxpair{B}{Y}\In \cat{D}`$

射 $`F`$ を依存ペアで書くのが都合が悪いときもあります。中置演算子記号は前置演算子記号としても使えるとして：

$`\quad (\odot)(F) = (\odot) F = \odot F`$

トータル射 $`F`$ への作用 $`(\odot)`$ の結果は次のプロファイル（域・余域）になります。

$`\quad \odot F : X\odot A \to Y\odot B \In \cat{D}`$

場合により、演算子記号を右肩（指数の位置）に付けることもあります。

$`\quad F^{\odot} : X\odot A \to Y\odot B \In \cat{D}`$

セクションとレトラクション

ファイブレーションを使う型理論では、ベース圏のセクション（または双対的にレトラクション）は重要な概念です。

ここでは圏 $`\cat{C}`$ はクラン〈clan〉だとします（「クラン、ファイブレーション、スパン」参照）。クランには、ファイブレーションクラス〈fibration class〉という射クラス〈class of morphisms | 射のクラス〉（「射のクラスと制約付きスパン // 圏の射のクラス」参照）が付随します。ファイブレーションクラスに属する射はファイブレーション〈fibration〉と呼びます。これは、ファイバー付き圏〈グロタンディーク・ファイブレーション〉とは別な概念です。クランのファイブレーションクラスは公理的・抽象的に規定される概念で、ファイブレーションの実体が何であるかは不定だし、別に何だっていいのです。

クランのファイブレーションを '$`\fibto`$' という矢印で表すことにします。包括圏とクランが一緒になった包括クラン（「テレスコープと包括クラン」参照）では、次のような標準的〈canonical | 規準的〉なファイブレーションがあります。

$`\quad X\cdot A \fibto X \In \cat{C}`$

クランのファイブレーションは射影とも呼びます。この“射影”もファイバー付き圏の射影（ファイバー付き圏そのもの）とは別な概念です。包括クランの標準射影〈canonical projection〉は両端（域と余域）で決まってしまうので、単に $`X\cdot A \fibto X`$ または $`X \fibot X\cdot A`$ と書きます。

$`\cat{C}`$ 内の標準射影のセクション〈section〉（「射影、入射、セクション、レトラクション」参照）達の集合を次のように書きます。

$`\quad \mrm{Sect}_\cat{C}(X \fibot X\cdot A) \subseteq \cat{C}(X, X\cdot A)`$

$`\mrm{Sect}_\cat{C}(X \fibot X\cdot A)`$ がなぜ重要かと言うと、セクションがインスタンスの概念を与えるからです。良い状況では、セクション達の集合をファイバー付き圏のトータル圏のホムセットに埋め込むことができます。（[追記]以下の埋め込みは怪しい、要確認。[/追記]）

$`\quad \mrm{Sect}_\cat{C}(X\cdot A \fibot X\cdot A\cdot B) \hookrightarrow \cat{D}(\ctxpair{A}{X},\ctxpair{B}{X\cdot A} )`$

包括クランの双対概念は余包括コクラン〈cocomprehension coclan〉です。コクランはコファイブレーションクラス〈cofibration class〉を持ちます。コクランのコファイブレーションを '$`\cofibto`$' という矢印で表すことにします。コファイブレーションは入射〈injection〉、埋め込み〈embedding〉とも呼びます。包括クランと同様に、余包括コクラン内の標準埋め込み〈canonical embedding〉は両端（域と余域）で決まります。

$`\quad X \cofibto X\cdot A \In \cat{C}`$

$`\cat{C}`$ 内の標準埋め込みのレトラクション〈retraction〉（「射影、入射、セクション、レトラクション」参照）達の集合を次のように書きます。

$`\quad \mrm{Retr}_\cat{C}(X\cdot A \cofibot X) \subseteq \cat{C}(X\cdot A, X )`$

良い状況では、レトラクション達の集合を余ファイバー付き圏〈反ファイブレーション〉のトータル圏のホムセットに埋め込むことができます。（[追記]以下の埋め込みは怪しい、要確認。[/追記]）

$`\quad \mrm{Retr}_\cat{C}(X\cdot A\cdot B \cofibot X\cdot A ) \hookrightarrow \cat{D}(\ctxpair{B}{X\cdot A}, \ctxpair{A}{X})`$

トータル射の結合公式と図示

$`\pi :\cat{D}\to \cat{C}`$ をファイブレーションとします。次のようなトータル射があるとします。

$`\quad F:\ctxpair{A}{X} \to \ctxpair{B}{Y} \In \cat{D}\\
\quad G:\ctxpair{B}{Y} \to \ctxpair{C}{Z} \In \cat{D}
`$

$`F, G`$ を依存ペアの形で書きます。

$`\quad F = \ctxpair{\alpha}{f} :\ctxpair{A}{X} \to \ctxpair{B}{Y} \In \cat{D}\\
\text{Where}\\
\quad f : X\to Y \In \cat{C}\\
\quad \alpha : A \to f^*B \In \cat{D}_{@X}
`$
$`\quad G = \ctxpair{\beta}{g} :\ctxpair{B}{Y} \to \ctxpair{C}{Z} \In \cat{D}\\
\text{Where}\\
\quad g : Y\to Z \In \cat{C}\\
\quad \beta : B \to g^*C \In \cat{D}_{@Y}
`$

$`f`$ を $`F`$ のベースパート〈base part〉、$`\alpha`$ を $`F`$ のファイバーパート〈fiber part〉と呼びます。$`G`$ に関しても同じです。

トータル射を図示するときは、関手 $`\pi`$ のなかに描く図式を利用します。

$`\quad \xymatrix{
A \ar[d]_\alpha
&{}
\\
{f^*B} \ar@{|->}[d]_\pi
&B \ar@{|->}[d]^\pi \ar@{|->}[l]_{f^*}
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi : \cat{D}\to \cat{C}
`$

$`\alpha`$ は縦方向ですが、関手 $`\pi`$ の値割り当て〈value assignment〉ではなくて $`\cat{D}_{@X}`$ の射（局所射）です。$`f^*`$ は $`\cat{D}@(f)`$ のことで、次のような関手です。

$`\quad f^* = \cat{D}@(f) \;: \cat{D}@(Y) \to \cat{D}@(X) \In \mbf{CAT}`$

トータル射 $`F, G`$ の結合は次の公式で計算できます。

$`\quad F;G = \ctxpair{\alpha}{f};\ctxpair{\beta}{g} = \ctxpair{\alpha; f^*\beta}{f;g}
`$

図示すると次のようです。

$`\quad \xymatrix{
{A} \ar[d]_\alpha \ar@/_1pc/[dd]_{\alpha ; f^* \beta}
&{}
&{}
\\
{f^* B} \ar[d]_{f^* \beta}
&{B} \ar[d]^{\beta} \ar@{|->}[l]_{f^*}
&{}
\\
{f^*(g^* C)} \ar@{|->}[d]_\pi
&{g^* C} \ar@{|->}[d]|\pi \ar@{|->}[l]_{f^*}
&{C} \ar@{|->}[d]^\pi \ar@{|->}[l]_{g^*}
\\
{X} \ar[r]_f \ar@/_1pc/[rr]_{f;g}
&{Y} \ar[r]_g
&{Z}
}\\
\quad \In \pi : \cat{D} \to \cat{C}
`$

最下段（4段目）はベース圏 $`\cat{C}`$ の対象・射で、それ以外はトータル圏 $`\cat{D}`$ の対象・射です。'$`\mapsto`$' の形の矢印は射ではなくて、対象に対する関手の値割り当てです。

おわりに

コンテキスタッドを、（包括圏と組み合わせて）型理論／論理／インスティチューション理論に応用するための基礎事項を、ファイブレーション〈ファイバー付き圏〉とファミリー〈インデックス付き圏〉を中心に述べました。漏れている事はあるでしょうが、それは必要に応じて補っていきます。

*1:局所射を垂直射〈vertical morphism〉と呼ぶことがあります。が、2-圏の垂直射と混同するので使わないほうがいいでしょう。

*2:[追記]$`a\in A, A\subseteq B`$ のとき、「$`a`$ は $`A`$ の要素か、$`B`$ の要素かどっちなんだ？どっちかに決めろ」と言われても困ります。[/追記]

*3:ここでの「局所」は「各対象ごとに」ですが、「各ホムセットごとに」の意味で「局所」を使うことがあります。「局所小圏」はその例です。