「型理論／論理／インスティチューション理論の引っ越し準備」の続きです。タイトルが長いので少し短くしました。「型理論など」は「型理論／論理／インスティチューション理論」のことです。
包括圏の変種（ある種の双対）や包括圏に対する付加的構造について述べて、インスタンス概念を表すハープーン射にも触れます。最後に、包括圏の使い方を示します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\twoto}{\Rightarrow}
\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
%\newcommand{\u}[1]{\underline{#1} }
\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
\newcommand{\In}{\text{ in } }
%\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\newcommand{\harto}{\rightharpoonup } % HARpoon TO
`$
内容：
包括圏と反包括圏
包括圏〈comprehension category〉は次の図式で記述できます。
$`\quad \xymatrix{
{\cat{C}} \ar@{=}[r]
&{\cat{C}}
\\
{\cat{E}} \ar[r]^\rho \ar[d]_\pi \ar[u]^\alpha
&{\mrm{Arr}(\cat{C}) } \ar[d]^{\mrm{Cod}} \ar[u]_{\mrm{Dom}}
\\
{\cat{C}} \ar@{=}[r]
&{\cat{C}}
}\\
\quad \text{strictly commutative }\In\mbf{CAT}
`$
ここで：
- $`\pi : \cat{E}\to \cat{C}`$ は、グロタンディーク・ファイブレーション
- $`\mrm{Arr}(\cat{C})`$ は、圏 $`\cat{C}`$ のアロー圏〈arrow category〉
- $`\mrm{Cod}: \mrm{Arr}(\cat{C})\to \cat{C}`$ は、アロー圏からの余域関手〈codomain functor〉、$`\mrm{Cod}`$ がグロタンディーク・ファイブレーションである必要はない。
- $`\rho : \cat{E}\to \mrm{Arr}(\cat{C})`$ は包括関手〈comprehension functor〉。$`\pi`$ のデカルト射を $`\mrm{Cod}`$ のデカルト射に移す（Cartesian morphism preserving）。
- $`\alpha : \cat{E}\to \cat{C}`$ は、コンテキスト拡張作用〈context extension action〉
- 図式は厳密可換なので、関手の等式が導かれる。
「コンテキスト拡張作用」は、次の正規表現のような同義語や省略があります。
{コンテキスト}?拡張{作用 | 演算 | 関手}?
グロタンディーク・ファイブレーション〈ファイバー付き圏〉を、グロタンディーク反ファイブレーション〈Grothendieck {opfibration | cofibration}〉に置き換えると反包括圏〈余包括圏 | {opcomprehensive | cocomprehensivi} category〉になります。図式は次のようです。
$`\quad \xymatrix{
{\cat{C}} \ar@{=}[r]
&{\cat{C}}
\\
{\cat{E}} \ar[r]^\rho \ar[d]_\pi \ar[u]^\alpha
&{\mrm{Arr}(\cat{C}) } \ar[d]^{\mrm{Dom}} \ar[u]_{\mrm{Cod}}
\\
{\cat{C}} \ar@{=}[r]
&{\cat{C}}
}\\
\quad \text{strictly commutative }\In\mbf{CAT}
`$
$`\mrm{Dom}, \mrm{Cod}`$ の位置が逆になっています。ここで：
- $`\pi : \cat{E}\to \cat{C}`$ は、グロタンディーク反ファイブレーション
- $`\mrm{Arr}(\cat{C})`$ は、包括圏のときと同じ
- $`\mrm{Dom}: \mrm{Arr}(\cat{C})\to \cat{C}`$ は、アロー圏からの域関手〈domain functor〉、$`\mrm{Dom}`$ がグロタンディーク反ファイブレーションである必要はない。
- $`\rho : \cat{E}\to \mrm{Arr}(\cat{C})`$ は反包括関手〈opcomprehension functor〉。$`\pi`$ の反デカルト射を $`\mrm{Dom}`$ の反デカルト射に移す（opCartesian morphism preserving）。
- $`\alpha : \cat{E}\to \cat{C}`$ は、包括圏のときと同じ（「反拡張」「余拡張」のような言い方はしない）。
- 図式は厳密可換なので、関手の等式が導かれる。
ベース圏 $`\cat{C}`$ の対象は、包括圏のときはコンテキスト、反包括圏のときは指標〈signature〉と呼びます。ただし、この呼び分けは守られないこともあります（割とイイカゲン）。
包括圏と反包括圏は、射の向きが逆になるだけで本質的な違いはありません。伝統や習慣に合わせて、どちらを使うかを決めます。型理論の伝統に合わせるなら包括圏、インスティチューション理論の伝統に合わせるなら反包括圏です。
上記の定義では、包括圏と反包括圏を一律に定義しましたが、実際には用語や記法が違ってきます。例えば、コンテキストは $`\Gamma`$ と書くことが多く、指標は $`\Sigma`$ と書くことが多いようです。また、僕の習慣ですが、反包括関手は $`\rho`$ ではなくて $`\iota`$ を使うことが多いです。本質的な違いはなくても、包括圏と反包括圏は（表面上は）だいぶ違った印象になるかも知れません。印象に惑わされないように。
クラン／コクラン
包括圏のグロタンディーク・ファイブレーションのベース圏 $`\cat{C}`$ （コンテキスト達の圏）は、単なる圏ではなくてクラン〈clan〉と仮定すると便利です。クランと包括圏については以下の過去記事達で述べています。
グロタンディーク反ファイブレーション（反包括圏）の場合は、クランの双対であるコクラン〈coclan〉を考えます。
クランのファイブレーションクラスとグロタンディーク・ファイブレーションが同じ「ファイブレーション」を使っている〈コンフリクトしている〉ので、混乱しないように注意してください。混乱の心配があるときは、単に「ファイブレーション」ではなくて、「グロタンディーク・ファイブレーション」（または「ファイバー付き圏」）と「クランのファイブレーション射」として区別します*1。クランのファイブレーション射はときに射影〈projection〉とも呼びます。コクランのコファイブレーション射はときに埋め込み〈embedding〉とも呼びます。
包括圏のベース圏はクラン、反包括圏のベース圏はコクランと常に仮定してよいでしょう。クランのファイブレーション射〈射影〉は $`\twoheadrightarrow`$ 、コクランのコファイブレーション射〈埋め込み〉は $`\rightarrowtail`$ で識別します。とはいえ、常にこの矢印を使うとは限りません。
包括圏のトータル射（$`\cat{E}`$ の射） $`\varphi`$ が（グロタンディーク・ファイブレーションの）デカルト射のとき：
- 包括関手の定義より、$`\rho(\varphi)`$ は、$`\mrm{Cod}`$ のデカルト射、つまり $`\cat{C}`$ のプルバック四角形になる（「余域関手のデカルト射はプルバック四角形」参照）。
反包括圏のトータル射 $`\varphi`$ が（グロタンディーク反ファイブレーションの）反デカルト射のとき：
- 反包括関手の定義より、$`\rho(\varphi)`$ は、$`\mrm{Dom}`$ の反デカルト射、つまり $`\cat{C}`$ のプッシュアウト四角形になる。
包括関手 $`\rho`$ による値 $`\rho(\varphi)`$ は次の形をしています（p.b. = pullback）。
$`\quad \xymatrix{
\cdot \ar[r] \ar@{->>}[d]
\ar@{}[dr]|{\text{p.b.} }
&\cdot \ar@{->>}[d]
\\
\cdot \ar[r]
&\cdot
}\\
\quad \In \cat{C}
`$
デカルト射 $`\varphi`$ に対するプルバック四角形 $`\rho(\varphi)`$ を、標準プルバック四角形〈canonical pullback square〉と呼びます。
反包括関手 $`\rho`$ による値 $`\rho(\varphi)`$ は次の形をしています（p.o. = pushout）。
$`\quad \xymatrix{
\cdot \ar[r] \ar@{>->}[d]
\ar@{}[dr]|{\text{p.o.} }
&\cdot \ar@{>->}[d]
\\
\cdot \ar[r]
&\cdot
}\\
\quad \In \cat{C}
`$
反デカルト射 $`\varphi`$ に対するプッシュアウト四角形 $`\rho(\varphi)`$ を、標準プッシュアウト四角形〈canonical pushout square〉と呼びます。
インデックス付き圏（宣言関手）
グロタンディーク・ファイブレーション $`\pi : \cat{E}\to \cat{C}`$ には、対応するインデックス付き圏 $`\msc{E}:\cat{C}^\op \to \mbf{CAT}\In 2\mbb{CAT}`$ があります。今ここでは、グロタンディーク・ファイブレーションと対応するインデックス付き圏を、フォントを変えた同じ文字で表しています（手書きだとこの方法は難しそう）。
$`\quad \cat{E} \longleftrightarrow \msc{E}`$
ファイブレーションのファイバーと、インデックス付き圏の値は同じ圏です。
$`\text{For }\Gamma \in |\cat{C}|\\
\quad \msc{E}(\Gamma) = \pi^{-1}(\Gamma) = \cat{E}_{@\Gamma}
`$
インデックス付き圏の値でもあるファイバー $`\cat{E}_{@\Gamma}`$ は、局所圏〈local category〉とも呼びます。
インデックス付き圏 $`\msc{E}`$ は、「型理論／論理／インスティチューション理論の引っ越し // 宣言」では宣言関手〈declaration functor〉と呼んだ関手です。局所圏の対象は宣言〈declaration〉とも呼びます -- が事例ごとに違う解釈と違う名前を持ちます。
宣言関手は、以前はエス関手〈ess functor〉と呼んでいた関手です。以下の過去記事達を参照。
インデックス付き圏（と呼ばれる反変関手）$`\msc{E}`$ の射パート $`\msc{E}_\mrm{mor}`$ の値（再インデキシング関手） $`\msc{E}(f) = \msc{E}_\mrm{mor}(f)`$ を $`f^*`$ と略記します。
包括圏のグロタンディーク・ファイブレーションに対応するインデックス付き圏〈宣言関手〉は、包括圏の一部として扱います。反包括圏のグロタンディーク反ファイブレーションに対応する余インデックス付き圏〈余宣言関手〉（共変関手）も同様に、反包括圏の一部とみまします。
余インデックス付き圏（と呼ばれる共変関手）$`\msc{F}`$ の射パート $`\msc{F}_\mrm{mor}`$ の値（再余インデキシング関手） $`\msc{F}(f) = \msc{F}_\mrm{mor}(f)`$ を $`f_*`$ と略記します。
宣言関手／余宣言関手は、一般的にはインデックス付き圏／余インデックス付き圏ですが、単純化したケースでは前層／余前層です。亜群〈groupoid〉達の圏に値を取る反変関手／共変関手である場合もあります。宣言関手／余宣言関手は意味論ではなくて、構文論の一部であることに注意してください（意味論の関手は別にある、「型理論周辺、何で混乱するのか？ // 構文論的意味論と意味論的意味論」参照）。
包括自然変換
「自然変換は関手」で述べたように、アロー圏への関手は自然変換を定義します。包括関手 $`\rho`$ から定義される自然変換を同じ名前で（オーバーロードして）$`\rho`$ とします。
$`\quad \rho:: \alpha \twoto \pi : \cat{E}\to \cat{C}\In \mbf{CAT}`$
この自然変換を包括自然変換〈comprehension natural transformation〉と呼びます。包括関手と包括自然変換は同じ情報を持っているので、どちらかひとつからもう一方を構成できます。
包括自然変換 $`\rho`$ の成分は次の形です。
$`\text{For }(\Gamma \mid A) \in |\cat{E}|\\
\quad \rho_{(\Gamma \mid A)} : \alpha(\Gamma \mid A)\to \pi(\Gamma \mid A)
\In \cat{C}
`$
$`\rho_{(\Gamma \mid A)} = \rho^{\Gamma, A}`$ と書いて、成分がクラン $`\cat{C}`$ のファイブレーション射〈射影〉であるという条件を付ければ、次の形に書けます。
$`\text{For }(\Gamma \mid A) \in |\cat{E}|\\
\quad \rho^{\Gamma, A} : \Gamma \cdot A \twoheadrightarrow \Gamma
\In \cat{C}
`$
自然変換の自然性四角形は次の形です。
$`\text{For }\varphi : (\Gamma \mid A) \to (\Delta\mid B) \In \cat{E}\\
\quad \xymatrix{
{\Gamma\cdot A} \ar[r]^{\alpha(\varphi)} \ar@{->>}[d]_{\rho^{\Gamma, A}}
&{\Delta\cdot B} \ar@{->>}[d]^{\rho^{\Delta, B}}
\\
\Gamma \ar[r]_{\pi(\varphi)}
&\Delta
}\\
\quad \text{commutative }\In \cat{C}
`$
一般的には、上記の可換四角形がプルバック四角形になるとは限りません。
包括関手の条件である「デカルト射を保存する」は、次の条件と同値です。
- トータル射 $`\varphi`$ が $`\pi`$ のデカルト射であるとき、$`\varphi`$ の自然性四角形はデカルト四角形〈プルバック四角形〉である。
もし、$`\cat{E}`$ の射がすべて$`\pi`$ のデカルト射であるなら、「デカルト射を保存する」は、次の条件と同値です。
- すべての自然性可換四角形がデカルト四角形〈プルバック四角形〉である。
型理論やインスティチューション理論で出てくるグロタンディーク・ファイブレーションでは、$`\cat{E}`$ の射がすべて$`\pi`$ のデカルト射になっていることが多いです。宣言関手が一般的なインデックス圏ではなくて、前層に限定することが多いからです。そのとき、グロタンディーク・ファイブレーションは離散ファイブレーションになります。離散ファイブレーションでは、すべてのトータル射がデカルト射です。
例えば、カートメル／ヴォエヴォドスキー〈John Cartmell, Vladimir Voevodsky〉のC-システム〈C-system〉は、離散ファイブレーションを定義するので、すべてのトータル射がデカルト射です。
C-システム（や類似の型理論的圏／インスティチューション理論的圏）に関しては、包括関手／包括自然変換の条件は次のようになります。
- 包括関手： すべてのトータル射 $`\varphi`$ に関して、$`\rho(\varphi)`$ はデカルト射である。
- 包括自然変換： すべてのトータル射 $`\varphi`$ に関して、自然性四角形はデカルト四角形〈プルバック四角形〉である。
現実的な型理論では、宣言関手に一般的なインデックス付き圏を使うことはオーバーキルになることがあります。C-システムがそうであるように、宣言関手は前層で、ファイブレーションは離散ファイブレーションである前提で議論するほうが話が単純化されます。しかし、例えばサブタイピング〈サブタイプ関係〉や論理の伴意〈エンテイルメント〉関係を扱う場合は、一般的なインデックス付き圏／一般的なグロタンディーク・ファイブレーションが必要なようです。
いずれにしても、トータル射（$`\cat{E}`$ の射）に非デカルト射があるかどうかに注意する必要があります。
拡張作用と厳密単位
「型理論／論理／インスティチューション理論の引っ越し準備 // 依存ペア」「型理論とコンテキスタッド： コンテキストフル射 // 依存ペアと作用演算」に書いたように、包括圏のトータル圏 $`\cat{E}`$ の対象である依存ペアの書き方はイッパイありますが、ここでは $`A = (\Gamma \mid A)`$ を使います。
包括圏の拡張作用を中置演算子記号で表すときは '$`\cdot`$' を使います。
$`\quad \alpha( (\Gamma\mid A) ) = \alpha(\Gamma \mid A) = \Gamma\cdot A`$
演算 $`\cdot`$ に対する厳密単位〈strict unit〉があると便利です。厳密単位を $`(\Gamma \mid \varepsilon)`$ と書きます。次が成立します。
$`\quad \alpha(\Gamma \mid \varepsilon) = \Gamma\cdot \varepsilon = \Gamma`$
厳密単位 $`\varepsilon`$ の実体は、次のようなセクション関手です（アスタリスクは関手の図式順結合演算子）。
$`\quad \varepsilon : \cat{C} \to \cat{E} \In \mbf{CAT}\\
\text{were }\\
\quad \varepsilon * \pi = \mrm{Id}_{\cat{C}}
`$
厳密単位律は、次の図式の厳密可換性です。
$`\quad \xymatrix{
\cat{E} \ar[dr]^{(\cdot)}
&{}
\\
\cat{C} \ar[u]^\varepsilon \ar[r]_{\mrm{Id}}
&{\cat{C}}
}\\
\quad \text{strictly commutative }\In \mbf{CAT}
`$
反包括圏の場合は、拡張作用の中置演算子記号は '$`+`$' を使います。$`\cdot`$ と双対な感じがするからです。
$`\quad \alpha( (\Gamma\mid A) ) = \alpha(\Gamma \mid A) = \Gamma + A`$
演算 $`+`$ に対する厳密単位は $`(\Gamma \mid \theta)`$ と書きます。次が成立します。
$`\quad \alpha(\Gamma \mid \theta) = \Gamma+ \theta = \Gamma`$
インスタンス＝ハープーン射
型理論のインスタンスの圏論的解釈については、「型理論へのファイブレーション的アプローチ： インスタンスとは // ハープーン」で述べています。ここでも、インスタンスとはハープーン射であると解釈します。
ハープーン射〈harpoon morphism〉とは、グロタンディーク・ファイブレーションのベース圏の対象〈ベース対象〉からトータル圏の対象〈トータル対象〉への射です。次の形で書きます。
$`\quad \psi : \Gamma \harto (\Delta \mid B)`$
もちろん、何の細工もなしにハープーン射を考えるのは無理です。ハープーン射の定義には幾つかの方法がありますが、厳密単位を仮定して次のように定義しましょう。
$`\quad \psi : \Gamma \harto (\Delta \mid B)
\iff \psi : (\Gamma\mid \varepsilon) \to (\Delta \mid B) \In \cat{E}
`$
つまり、ハープーン射は特殊な形のトータル射です。
この定義だと、ハープーン射の前にベース射を結合すること、ハープーン射の後にトータル射を結合することは自明に定義できます。トータル射の特別な場合として局所射〈垂直射〉を後結合〈ポスト結合〉できます。
特別な形のハープーン射 $`\psi : \Gamma \harto (\Gamma \mid A)`$ は、次のトータル射です。
$`\quad \psi : (\Gamma\mid \varepsilon) \to (\Gamma \mid A) \In \cat{E}`$
これは（$`\Gamma`$ 上の）局所射となるので、この形のハープーン射は局所ハープーン射〈local harpoon morphism〉と呼ぶことにします。
インスタンス〈instance〉はハープーン射と同義だとします。局所インスタンス〈local instance〉は局所ハープーン射と同義です。局所インスタンスは、厳密単位から出る局所射です。
インスタンスのコンテキスト〈context of an instance〉とは、ハープーン射としての域（ベース対象と考える）のことで、インスタンスの型〈type of an instance〉とは、ハープーン射としての余域（トータル対象と考える）のことです。
インスタンス $`\psi : \Gamma \harto (\Delta \mid B)`$ は、コンテキスト $`\Gamma`$ 上の型 $`(\Delta\mid B)`$ のインスタンスです。あるいは、コンテキスト $`\Gamma`$ から型 $`(\Delta\mid B)`$ へのインスタンスです。
ベース圏 $`\cat{C}`$ がクランだとすると、クランの条件から特定された終対象を持ちます。この終対象を $`\diamond`$ と書きます。$`\diamond`$ からのインスタンスを大域インスタンス〈global instance〉と呼びます。大域インスタンスのなかには、$`\diamond`$ 上の局所インスタンス（以下の形）が含まれることに注意してください。
$`\quad \psi : \diamond \harto (\diamond \mid A)`$
上の形のインスタンスは大域局所インスタンス〈global local instance〉です。
型理論では、一般的なトータル射よりインスタンス、つまりハープーン射に注目します。包括関手とコンテキスト拡張を道具として、インスタンス〈ハープーン射〉について調べることが、型理論〈圏論的依存型理論〉の主要な目的と言っていいでしょう。
包括圏の使い方
型理論／論理／インスティチューション理論などにおいて包括圏を使う場合は、グロタンディーク・ファイブレーションのもとになるインデックス付き圏からスタートするのが良いでしょう。インデックス付き圏は次の形になります。
$`\quad \msc{E}: \cat{C}^\Box \to \cat{V}`$
右肩の $`\Box`$ には、$`\op`$ が入るか、あるいは何も入りません。これは、$`\msc{E}`$ をインデックス付き圏〈反変関手〉にするか余インデックス付き圏〈共変関手〉にするかの選択です。反変関手を選べば包括圏を使うことになり、共変関手を選べば反包括圏を使うことになります。
関手（反変関手または共変関手）の余域〈ターゲット圏〉$`\cat{V}`$ の選択肢には次のようなものがあります。
- $`\mbf{Set}`$
- $`\mbf{Ord}`$
- $`\mbf{Gpd}`$
- $`\mbf{Cat}`$
- $`\mbf{CartCat}`$ （デカルト圏達の2-圏）
- $`\mbf{CCCat}`$ （デカルト閉圏達の2-圏）
上記はいずれも、対象が小さい構造である圏／2-圏です。より大きなサイズの構造が必要なら、$`\mbf{SET}, \mbf{ORD}, \cdots`$ などを使います。
ターゲット圏が2-圏になると、関手の種類が厳密関手・スード関手・ラックス関手・反ラックス関手などがあるので、その種類を選ぶ必要があります。
ベースになるインデックス付き圏／余インデックス付き圏が決まれば、対応するグロタンディーク・ファイブレーションは自動的に決まります。そのグロタンディーク・ファイブレーションに対して何かしらの包括関手／余包括関手、あるいは包括自然変換／余包括自然変換を選びます。包括構造を決めれば、拡張作用は自動的に決まります。
包括圏／反包括圏の構成には非常の多くの選択肢〈オプション〉があります。これは、オプションの設定によって、相当に広い範囲をカバーできることでもあります。型理論／論理／インスティチューション理論などの引っ越し先として、包括圏とコンテキスタッドの枠組みは十分なものだと言えるでしょう。
*1:さらにややこしいことには、圏達の2-圏は、グロタンディーク・ファイブレーションをファイブレーション射とした（大きくて2次元の）クランの構造を持ちます。
