あー、そういうことかぁ！
僕は、用語の語源にあまりこだわらないので、「包括圏」の語源は知らなかったし、調べることもしませんでした。「なんでか知らんけど、『包括圏』って呼ぶのね」で済ませていました。語源や逸話を知らないと概念を理解できないわけではないので、「なんでか知らんけど」で済ませるのもまー健全な態度でしょう（と思ってます）。
最近、“いわゆる包括”から包括圏が作れることに気付いて語源・由来の察しが付きました。“いわゆる包括”の事例は、語源うんぬんの話は別にしても示唆的で包括圏の良い例なので紹介します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#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{\incto}{\hookrightarrow }
\newcommand{\LLE}{\sqsubseteq } % Logical Less or Equal
`$
内容：
包括とは
集合 $`X`$ 上に述語 $`p`$ があると、$`p`$ を満たす $`X`$ の要素達からなる部分集合が特定できます。この部分集合は次のように書きます。
$`\quad \{x\in X\mid p(x)\}`$
これはお馴染みですよね。この書き方は、部分集合の内包的定義〈intensional subset definition | intensional definition of a subset〉と言ったりします。
包括〈comprehension〉は内包〈intension〉とほぼ同義語です。ニュアンスの違いがあるのかも知れませんが、僕は微妙な違いは知りません。comprehension の翻訳語として（「包括」ではなくて）「内包」を使うこともあるので、包括と内包を区別しなくても大丈夫でしょう。
包括（あるいは内包）による部分集合の定義は、条件を指定して部分集合の要素を選び出すやり方です。このやり方で部分集合が特定できることを包括公理〈axiom {schema}? of comprehension〉と呼ぶことがあります。ただし、最近は分出公理〈axiom {schema}? of separation〉という呼び名がメジャーで「包括公理」が使われることは稀です*1。英語では axiom {schema}? of separation より axiom {schema}? of specification のほうが多い印象です。
ここでの包括〈comprehension〉とは、全体集合 $`X`$ とその上の述語 $`p`$ から部分集合 $`\{x\in X\mid p(x)\}`$ を作る行為、あるいはそうやって作った部分集合のことだとします。
写像と部分集合の標準プルバック四角形
写像〈関数〉$`f:X \to Y`$ に対して、次の記法を使うことにします。
- 部分集合 $`A\subseteq X`$ の像集合は $`f(A)`$ と書く。同じ記号 $`f`$ をオーバーロード〈多義的使用〉する。
- 部分集合 $`B\subseteq Y`$ の逆像集合は $`f^{-1}(B)`$ と書く。逆写像と同じ記号 $`f^{-1}`$ をオーバーロードする。
- $`f`$ を、部分集合 $`A\subseteq X`$ に制限した写像を $`f|_A : A \to Y`$ と書く。
- $`f(A)\subseteq B`$ であるとき、$`f|_A`$ の余域を $`B`$ に制限した写像を $`f|_A^B : A \to B`$ と書く。
- 文脈から、部分集合 $`A, B`$ が明らかなら、$`f|_A`$ や $`f|_A^B`$ を単に $`f|`$ と書く。
上記の約束に従って、$`f`$ と $`f|`$ の状況を図式にすると次のようです。
$`\quad \xymatrix{
A \ar@{_{(}->}[d] \ar[r]^{f|}
\ar@{}[dr]|{\text{comm.}}
&B \ar@{_{(}->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \mbf{Set}
`$
ここで、'$`\incto`$' の形の矢印は包含写像（部分集合の埋め込み）です。四角形内の $`\text{comm.}`$ は、その四角形が可換四角形〈commutative square〉であることを示します。この図なら、可換四角形は以下の等式と同じことです。以下の $`\mrm{incl}_\hyp^\hyp`$ は包含写像のこと、セミコロンは図式順結合記号〈diagrammatic-order composition symbol〉です。
$`\quad \mrm{incl}_A^X ; f = f| ; \mrm{incl}_B^Y`$
この可換四角形において、$`A = f^{-1}(B)`$ と置くと、単なる可換四角形ではなくてプルバック四角形になります。四角形内の $`\text{p.b.}`$ がプルバック四角形であることの目印です。
$`\quad \xymatrix{
{f^{-1}(B)} \ar@{_{(}->}[d] \ar[r]^{f|}
\ar@{}[dr]|{\text{p.b.}}
&B \ar@{_{(}->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \mbf{Set}
`$
つまり、逆像集合 $`f^{-1}(B)`$ は、$`f`$ と $`\mrm{incl}_B^Y`$ のファイバー積として与えられます。
上記のプルバック四角形を、写像〈関数〉$`f`$ と部分集合 $`B`$ に関する標準プルバック四角形〈canonical pullback square〉と呼ぶことにします。実際これは、包括圏の標準プルバック四角形になります。
包括の標準プルバック四角形
二元集合 $`\{0, 1\}`$ を真偽値集合だとして、集合 $`X`$ 上の述語〈predicate〉達の集合を次のように書きます。
$`\quad \mrm{Pred}(X) := \mrm{Map}(X, \{0, 1\})`$
集合 $`\mrm{Map}(X, \{0, 1\})`$ にブール代数（述語達のブール代数）の構造を持たせることができますが、ここでは論理的な順序構造（$`0 \le 1`$ に基づく順序）だけを考えます。順序集合としての $`\mrm{Pred}(X)`$ を、次のように書きます。
$`\quad \mrm{Pred}(X) = (|\mrm{Pred}(X)|, \LLE)`$
$`|\mrm{Pred}(X)|`$ は、順序集合の台集合ですが、順序集合をやせた圏とみなすので、圏の対象集合〈the set of objects〉の記号を使っています。ただし、通常の扱いでは、通常の記号の乱用を使って $`\mrm{Pred}(X)`$ と $`|\mrm{Pred}(X)|`$ の区別はしません。
写像 $`f:X \to Y`$ に対して、順序集合のあいだの写像（順序を保存する写像） $`\mrm{Pred}(f)`$ を次のように定義します。
$`\quad \mrm{Pred}(f) : \mrm{Pred}(Y)\to \mrm{Pred}(X)\In \mbf{Ord}\\
\text{For } q\in \mrm{Pred}(Y)\\
\quad \mrm{Pred}(f)(q) := f;q = q\circ f = \lambda\, x\in X. q(f(x))
`$
$`\mrm{Pred}(\hyp)`$ は、次のような反変関手になります。以下で、$`\mbf{Ord}`$ は順序集合達の圏です。
$`\quad \mrm{Pred} : \mbf{Set}^\op \to \mbf{Ord}\In \mbf{CAT}`$
$`\mrm{Pred}(f)`$ を $`f^*`$ と略記することにします。繰り返し定義を書けば：
$`\quad f^* : \mrm{Pred}(Y)\to \mrm{Pred}(X)\In \mbf{Ord}\\
\text{For } q\in \mrm{Pred}(Y)\\
\quad f^*(q) := f;q = q\circ f = \lambda\, x\in X. q(f(x))
`$
さて、包括〈内包〉により定義した部分集合は $`\{x\in X\mid p(x)\}`$ と書きますが、変数 $`x`$ はなくても同じなので、$`\{X\mid p \}`$ とも書きます。$`\{X\mid p \}`$ は、集合 $`X`$ と述語 $`p`$ から包括により定義された部分集合、あるいは短く、$`X`$ と $`p`$ の包括〈comprehension of $`X`$ and $`p`$〉です。
前節の標準プルバック四角形を、包括により書き換えると次のようになります。
$`\quad \xymatrix{
{\{ X\mid f^*(q)\}} \ar@{_{(}->}[d] \ar[r]^{f|}
\ar@{}[dr]|{\text{p.b.}}
&{ \{Y \mid q\}} \ar@{_{(}->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \mbf{Set}
`$
これを、包括の標準プルバック四角形〈canonical pullback square of a comprehension〉と呼ぶことにします。前節の“写像 $`f`$ と部分集合 $`B`$ の標準プルバック四角形”の $`B`$ を、包括 $`\{Y\mid q\}`$ で置き換えたものです。
包括圏
包括圏については以下の過去記事に書いています。
ここで、必要なことを手短に繰り返します。
包括圏の構成素〈constituent〉達を一枚の図式で描くと次のようです。
$`\quad \xymatrix{
{}
&{\cat{C}}
\\
{\cat{D}} \ar[r]^H \ar[ur]^{(\cdot)} \ar[dr]_{\pi}
&{\mrm{Arr}(\cat{C})} \ar[d]^{\mrm{Dom}} \ar[u]_{\mrm{Cod}}
\\
{}
&{\cat{C}}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
$`\pi`$ はファイブレーション〈ファイバー付き圏〉の射影です。$`(\cdot)`$ は特に条件はない関手です。$`(\cdot)`$ という奇妙な書き方については「包括コンテキスタッドに向けて // 中置演算子記号の使い方」を参照してください。$`\mrm{Arr}(\cat{C})`$ はアロー圏です。アロー圏については「アロー圏 ＝ バンドルの圏」を見てください。関手 $`H`$ は包括圏の包括関手〈comprehension functor〉と呼びます。$`H`$ には「デカルト射を保存する」という条件が付きます。デカルト射については「関手のデカルト射とファイバー付き圏」に書いています。
上の図式の一部を取り出して90度回転して描くと：
$`\quad \xymatrix{
{}
&{\cat{D}} \ar[dl]_{\pi} \ar[dr]^{(\cdot)}
&{}
\\
{\cat{C}}
&{}
&{\cat{C}}
}\\
\quad \In\mbf{CAT}
`$
これは、$`\mbf{CAT}`$ 内の自己スパン〈endo-span〉です。
アロー圏 $`\mrm{Arr}(\cat{C})`$ への関手 $`H`$ は自然変換を定義します（「自然変換は関手」参照）。その自然変換を $`\rho`$ とすると、以下のようです。
$`\quad \xymatrix{
{\cat{D}} \ar@/_1pc/[d]_{\pi} \ar@/^1pc/[d]^{(\cdot)}
\ar@{}[d]|{\overset{\rho}{\Leftarrow}}
\\
{\cat{C}}
}\\
\quad \In\mbf{CAT}
`$
図ではなくテキストで書くなら：
$`\quad \rho :: (\cdot) \twoto \pi : \cat{D}\to \cat{C}\In \mbf{CAT}`$
関手 $`H`$ に対応する自然変換 $`\rho`$ を包括自然変換〈comprehension natural transformation〉と呼びます。包括自然変換は、デカルト自然変換〈Cartesian natural transformation〉です。デカルト自然変換 $`\rho`$ の自然性可換四角形〈naturality commutative square〉が、包括圏の標準プルバック四角形〈canonical pullback square〉です。
カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉に倣って、トータル圏 $`\cat{D}`$ の対象を $`\ctxpair{A}{X}`$ と書くことにして、$`\rho`$ の自然性可換四角形は以下のようです。
$`\text{For }F : \ctxpair{A}{X} \to \ctxpair{B}{Y} \In \cat{D}\\
\quad \xymatrix{
{(\cdot)(\ctxpair{A}{X}) } \ar[d]_{\rho_{\ctxpair{A}{X}}} \ar[r]^{(\cdot)(F)}
\ar@{}[dr]|{\text{p.b.}}
&{(\cdot)(\ctxpair{B}{Y}) } \ar[d]^{\rho_{\ctxpair{B}{Y}}}
\\
{\pi(\ctxpair{A}{X}) } \ar[r] \ar[r]_{\pi(F)}
&{\pi(\ctxpair{B}{Y}) }
}\\
\quad \In \cat{C}
`$
見にくいので、次の書き換えをします。
- $`(\cdot)`$ を中置演算子記号に書き換える。
- $`\rho_{\ctxpair{A}{X}}`$ は $`\rho_A^X`$ に書き換える。
- $`\pi(\ctxpair{A}{X})`$ は $`X`$ に書き換える。
- $`\pi(F) = f`$ と置く。
- $`(\cdot)(F)`$ は、他の射達から決まるので無名とする。
すると：
$`\quad \xymatrix{
{X\cdot A } \ar[d]_{\rho_X^A } \ar[r]
\ar@{}[dr]|{\text{p.b.}}
&{Y\cdot B } \ar[d]^{\rho_Y^B}
\\
{X } \ar[r]_f
&{Y }
}\\
\quad \In \cat{C}
`$
プルバック四角形であるためには、$`A`$ と $`B`$ を勝手に取れるわけではありません。ファイブレーションに対応するインデックス付き圏の再インデキシング関手を $`f^*`$ とすると、
$`\quad A = f^*(B)`$
という条件で縛られます。この条件を加味すると、プルバック四角形はさらに次のように書き換えられます。
$`\quad \xymatrix{
{X\cdot f^*(B) } \ar[d]_{\rho_X^{f^*(B)} } \ar[r]
\ar@{}[dr]|{\text{p.b.}}
&{Y\cdot B } \ar[d]^{\rho_Y^B}
\\
{X } \ar[r]_f
&{Y }
}\\
\quad \In \cat{C}
`$
包括から作る包括圏
通常、包括圏は、型理論の構文論的構造の圏論的な定式化として使われますが、“いわゆる包括”から作る包括圏は論理の意味論的構造の圏論的な定式化になっています*2。集合とその上の述語を扱っているので、包括から作る包括圏はハイパードクトリンにかなり近いものです。
最初の3つの節で述べた“いわゆる包括”から、どのようにして包括圏を作るかの概略を以下に述べます。抽象的な包括圏の構成素達が、どのように具体化されるかというと：
- 包括圏のベース圏は、集合圏。 $`\cat{C} := \mbf{Set}`$
- 包括圏のトータル圏は、述語の圏。 $`\cat{D} := \int_{\mbf{Set}} \mrm{Pred}`$ （グロタンディーク構成）
- 包括圏の射影は、グロタンディーク構成の射影。
$`\pi := \pi_{\mrm{Pred}} : \int_{\mbf{Set}}\mrm{Pred} \to \mbf{Set} \In \mbf{CAT}`$ - 包括圏の作用は、包括。 $`(\cdot)(\ctxpair{p}{X} ) = X\cdot p := \{X\mid p\}`$
- 包括圏の包括自然変換は、包含射〈包含写像〉の族。 $`\rho_X^p := \mrm{incl}_X^p := \mrm{incl}_{\{X\mid p\}}^X`$
幾つかの補足をします。
グロタンディーク構成は圏論では頻出する構成です。以下の過去記事を参照してください。
グロタンディーク構成の結果はファイブレーション〈ファイバー付き圏〉であり、ファイブレーションのトータル圏は平坦化圏〈flattened category | 狭義のグロタンディーク構成〉で与えられます。トータル圏の対象は、ベース圏のどれかの対象 $`X`$ 上のファイバー〈局所圏〉$`\cat{D}_{@X}`$ の対象です。このことを次のように表します。
$`\quad A = \ctxpair{A}{X} \in |\cat{D}_{@X}|`$
今の事例では、ファイバー〈局所圏〉とは、述語達の順序集合 $`\mrm{Pred}(X)`$ をやせた圏とみなしたものです。よって：
$`\quad q = \ctxpair{q}{X} \in |\mrm{Pred}(X)|`$
包含射の族（の成分）$`\mrm{incl}_X^p`$ は行きがかり上、最初に出した $`\mrm{incl}_A^X`$ の形とは、添字の上下が逆になってしまいました。$`\mrm{incl}_X^p`$ は以下のような自然変換 $`\mrm{incl}`$ の成分です。
$`\quad \mrm{incl} :: (\cdot) \twoto \pi : \int_{\mbf{Set}}\mrm{Pred} \to \mbf{Set}\In \mbf{CAT}`$
自然変換 $`\mrm{incl}`$ はデカルト自然変換なので、その自然性可換四角形は以下のようなプルバック四角形になります。$`\mrm{incl}`$ の成分は $`\incto`$ の矢印で書きます。
$`\quad \xymatrix{
{X\cdot f^* q} \ar[r] \ar@{_{(}->}[d]
\ar@{}[dr]|{\text{p.b.}}
&{Y\cdot q} \ar@{_{(}->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \mbf{Set}
`$
$`{X\cdot f^* q} = \{X\mid f^*p\}, {Y\cdot q} = \{Y\mid q\}`$ だったので、このプルバック四角形は次のようです。
$`\quad \xymatrix{
{ \{X\mid f^* q\}} \ar[r] \ar@{_{(}->}[d]
\ar@{}[dr]|{\text{p.b.}}
&{\{Y\mid q\} } \ar@{_{(}->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \mbf{Set}
`$
これはまさに、“いわゆる包括”の標準プルバック四角形です。
包括圏のキモは包括自然変換の自然性可換四角形として現れる標準プルバック四角形なので、それが“いわゆる包括”から生じていることを観察できれば十分でしょう。詳細はともかくとして、“いわゆる包括”から包括圏が作れたのです。
おわりに
“いわゆる包括”が包括圏を定義することは、以下のナジメイ／ヴァン・デル・ワイド／アーレンス／ノースの論文のなかでトポスでの例が出ており、一般のトポスを集合圏に具体化したものをこの記事で紹介しました。
- [NWAN25-]
- Title: A Type Theory for Comprehension Categories with Applications to Subtyping
- Authors: Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
- Submitted: 13 Mar 2025
- Pages: 32p
- URL: https://arxiv.org/abs/2503.10868
包括から作られた包括圏の局所圏〈ファイバー〉は離散圏〈集合〉ではありませんが、やせた圏〈順序集合〉なので比較的単純です。標準プルバック四角形は、内包的に定義された部分集合の逆像の構成に対応するので、これも比較的理解しやすいと思います。型理論の知識は要らないので、包括圏の近づきやすい例になっています。また、包括から作られた包括圏は、論理を包括圏のなかで展開するときに参考になります。
包括から作られた包括圏は、型理論的な包括圏とは出自が違うので、型理論的包括圏で成立していたこと（例えばベース圏がクランであること）が成立しません。このことは、型理論以外における包括圏も考えるきっかけになります。型理論以外でも包括圏を使える場面がありそうです。
