æ‹¡å¼µåŒ…æ‹¬æ§‹é€ ã®ã‚‚ã†ã²ã¨ã¤ã®å®šå¼åŒ–

拡張包括構造については、「最近の型理論： 拡張包括構造を持ったインデックス付き圏」で述べたことがあります。型理論的圏（「指標の圏はコンテキストの圏の反対圏」参照）は、なんらかの拡張包括構造を持ちます。

拡張包括構造の定式化は色々とあります。ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉は、拡張包括構造を抽象度が高い簡潔な形に定式化した型理論的圏です。比較的に具体的であるカートメル構造（「パルムグレンによる、型理論の複前層モデル // カートメル構造」参照）も、潜在的に拡張包括構造を含んでいます。

この記事では、圏 $`\mathcal{C}`$ 上の拡張包括構造を、ステップとディスプレイという2つの前層を中心に定式化してみます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in }}
%\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
%\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\op}{ \mathrm{op} } % used
\newcommand{\hyp}{\text{－} } % used
\newcommand{\id}{ \mathrm{id} } % used
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\twoto}{ \Rightarrow } % used
\newcommand{\ILT}{ \triangleleft } % immediately less than
\newcommand{\IGT}{ \triangleright } % immediately greater than
\newcommand{\MC}[1]{ \mathscr{#1} } % Morphism Class
`$

ディスプレイ射とディスプレイ前層

「パルムグレンによる、型理論の複前層モデル // カートメル構造」において、ディスプレイ射は標準射影射の同義語として導入しました。ここでは、圏 $`\cat{C}`$ に最初から備わっている射のクラス（「射のクラスと制約付きスパン // 圏の射のクラス」参照）としてディスプレイ射のクラスを考えます。ディスプレイ射は公理的に与えられる概念なので、導入時に「ディスプレイ射とは何であるか」には言及しません。

射のクラスは筆記体〈スクリプト体〉大文字で表すことにします。$`\MC{D}`$ を、圏 $`\cat{C}`$ の射のクラスとします。

$`\quad \MC{D} \subseteq \mrm{Mor}(\cat{C})`$

射のクラス $`\MC{D}`$ がファイバー引き戻しに関して閉じている〈closed under fiber pullbacks〉、または安定している〈stable under fiber pullbacks〉とは、以下のことです； 次の形のコスパンを考えます。

$`\quad \xymatrix{
{}
& \cdot \ar[d]^{d}
\\
\cdot \ar[r]_f
&\cdot
} \In \cat{C}\\
\text{Where}\\
\quad d \in \MC{D}\\
\quad f \in \mrm{Mor}(\cat{C})
`$

このような $`d, f`$ に対して、極限錐（プルバック四角形と言っても同じ）が存在し、$`d`$ の対辺の射（後で $`f^\# d`$ と書く）が再び $`\MC{D}`$ に属するなら、$`\MC{D}`$ はファイバー引き戻しに関して閉じています。

ファイバー引き戻しに関して閉じた射のクラスをディスプレイ射のクラス〈class of display {maps | morphisms}〉、あるいはディスプレイクラス〈display class〉と呼びます。ディスプレイクラスの要素がディスプレイ射〈display {map | morphism}〉です。そして、ディスプレイクラスを備えた圏 $`(\cat{C}, \MC{D})`$ を、ディスプレイクラス付き圏〈category with display class〉 と呼びます。

$`(\cat{C},\MC{D})`$ をディスプレイクラス付き圏とすると、上記のようなスパン $`d, f`$ に対してプルバック四角形は存在します。ひとつのプルバック四角形を選んで、$`f^\# d`$ を以下のような射だと定義します。

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

$`d, f`$ に対して $`f^\# d`$ が一意的に決まるわけではなくて、プルバック四角形の選び方にも依存します。ディスプレイクラスの定義から、$`f^\# d`$ はディスプレイ射（ディスプレイクラス $`\MC{D}`$ の要素）です。

$`(\cat{C},\MC{D})`$ と、選択した $`(d, f) \mapsto f^\# d`$ 達により、対応 $`\mrm{Disp}(\hyp)`$ を定義します。

• $`X\in |\cat{C}|`$ に対して、$`\mrm{Disp}(X) := \{d\in \MC{D}\mid \mrm{cod}(d) = X\}`$ と定義する。
• $`f:X \to Y \In \cat{C}`$ に対して、写像 $`\mrm{Disp}(f) : \mrm{Disp}(Y) \to \mrm{Disp}(X) \In {\bf Set}`$ を、$`\mrm{Disp}(f)(d) := f^\# d`$ と定義する。

このように定義した $`\mrm{Disp}`$ は、$`\cat{C}`$ の対象に集合、射に写像を（逆向きに）対応させます。しかし、反変関手である保証はありません。$`\mrm{Disp}`$ が関手になるとき、選択した $`(d, f) \mapsto f^\# d`$ 達を、ディスプレイクラス $`\MC{D}`$ の分裂子〈splitting〉と呼びます。

分裂子を持つディスプレイクラスを分裂可能〈splittable〉、分裂可能なディスプレイクラスと“特定された分裂子”の組を分裂ディスプレイクラス〈split display class〉と呼びます。分裂ディスプレイクラスは反変関手 $`\mrm{Disp}`$ を定義します。「分裂子」「分裂可能」「分裂」は、ファイバー付き圏の用語を流用しています。

集合圏への反変関手は前層なので、分裂ディスプレイクラス $`\MC{D}`$ から作られた $`\mrm{Disp}`$ は前層です。この前層を（$`\MC{D}`$ の）ディスプレイ前層と呼びます。

ステップ集合とステップ前層

圏 $`\cat{C}`$ にカートメル構造（「パルムグレンによる、型理論の複前層モデル // カートメル構造」参照）が在ると、2つの対象のあいだの拡張関係〈extension relation〉が定義できます。$`Y`$ が $`X`$ の拡張〈直接拡張〉であることは次のように書きます。

$`\quad X \ILT Y`$

カートメル構造では、「拡張になっている」という静的状況を記述していますが、「拡張する」という行為を動的に記述しているわけではありません。対象を拡張する1ステップの行為、あるいはリストの末尾への項目追加の行為を $`\mrm{Step}(\hyp)`$ という対応で表現しましょう。

• $`X\in |\cat{C}|`$ に対して、$`\mrm{Step}(X)`$ という集合が対応している。この集合の要素を拡張ステップ〈extension step〉、あるいは単にステップ〈step〉と呼ぶ（解釈は後述）。
• $`f:X \to Y \In \cat{C}`$ に対して、写像 $`\mrm{Step}(f) : \mrm{Step}(Y) \to \mrm{Step}(X) \In {\bf Set}`$ という写像が対応している。
• $`\mrm{Step}`$ は反変関手になっている。

$`\mrm{Step}`$ は集合圏への反変関手なので前層です。ステップ前層〈step presheaf〉と呼ぶことにします（[追記]後の記事「コンテキストの圏と指標の圏と限量子」では、ステップ前層の一般化をエス関手と呼んでいます。）[/追記]）。$`\mrm{Step}`$ は、名前は「ステップ」ですが、定義上は単なる前層です。今のところ、前層以外の条件は付きません。

$`\cat{C}`$ がカートメル構造を持つ圏のとき、$`\mrm{Step}`$ を次のように定義できます。

• $`X\in |\cat{C}|`$ に対して、$`\mrm{Step}(X) := \{X' \in |\cat{C}| \mid X \ILT X' \}`$
• $`f:X \to Y \In \cat{C}`$ に対して、$`\mrm{Step}(f)(Y')`$ は標準プルバック四角形により与えられる $`X'`$ と定義する。

標準プルバック四角形については「パルムグレンによる、型理論の複前層モデル // カートメル構造」を参照してください。

分裂ディスプレイクラスから定義される $`\mrm{Disp}`$ も前層なので、ステップ前層となります。今は、前層であれば、何でも「ステップ前層」ということになりますが、次節以降で条件を付けます。

拡張自然変換

$`(\cat{C}, \MC{D})`$ が分裂ディスプレイクラス付き圏とします。$`\mrm{Disp}`$ は分裂子に対応するディスプレイ前層とします。もうひとつの $`\cat{C}`$ 上の前層 $`\mrm{Step}`$ があり、次のような自然変換 $`\rho`$ があるとします。

$`\quad \rho :: \mrm{Step} \twoto \mrm{Disp} : \cat{C}^\op \to {\bf Set} \In {\bf CAT}`$

$`\rho`$ の自然性四角形は次のようになります。

$`\text{For } f: X \to Y \In \cat{C}\\
\quad \xymatrix{
\mrm{Step}(X) \ar[r]^{\rho_X}
& \mrm{Disp}(X)
\\
\mrm{Step}(Y) \ar[r]_{\rho_Y} \ar[u]^{\mrm{Step}(f)}
& \mrm{Disp}(Y)\ar[u]_{\mrm{Disp}(f)}
}\\
\quad \text{commutative }\In {\bf Set}
`$

次のような記法の約束をします。

• 集合 $`\mrm{Step}(X)`$ の要素 $`A`$ を、 $`(X, A)`$ のような依存ペアとしても書く。
• $`\mrm{Step}(f)`$ の $`B \in \mrm{Step}(Y)`$ への作用（の結果）を $`f^* B \in \mrm{Step}(X)`$ と書く。
• å°„ $`\rho_X(A) = \rho_X( (X, A) )`$ の域を $`X\cdot A`$ と書き、次の記法を使う。
  $`\rho_X( (X, A) ) = (\rho^{X, A} : X\cdot A \to X)`$

すると、上の自然性四角形の要素を追いかけた図式は次のように書けます。

$`\quad \xymatrix{
(X, f^* B) \ar@{|->}[r]^-{\rho_X}
& (\rho^{X, f^* B} : X\cdot f^* B \to X)
\\
(Y, B) \ar@{|->}[r]_-{\rho_Y} \ar@{|->}[u]^{\mrm{Step}(f)}
& (\rho^{Y, B}:Y\cdot B \to Y) \ar@{|->}[u]_{\mrm{Disp}(f)}
}
`$

上の図式の情報を、描き方を少し変えて描いてみると：

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

ここで、$`f^* B`$ はステップ $`B`$ の $`f`$ に沿った引き戻し（反変関手 $`\mrm{Step}`$ による逆向き作用）、$`\cdot`$ は対象を拡張する演算、$`\rho^\hyp`$ は拡張に伴う標準射影で、ディスプレイ射になっている、という状況です。

関手 $`\mrm{Disp}`$ は、ディスプレイ射と任意の射（のコスパン）に対して、選択された標準プルバック四角形を対応させるので、その標準プルバック四角形は次のように書けます。

$`\quad \xymatrix{
{f^\# (Y \cdot B)} \ar[r]^{f^\uparrow} \ar[d]_{f^\# (\rho^{Y, B})}
\ar@{}[rd]|{\text{p.b.}}
& {Y\cdot B} \ar[d]^{\rho^{Y, B}}
\\
X \ar[r]_f
& Y
}\\
\quad \In \cat{C}
`$

$`f^\#`$ はファイバー引き戻しを表します。

先の図式と今の図式を比較すると次が言えます。

$`\quad f^\#(Y\cdot B) = X\cdot f^* B\\
\quad f^\# (\rho^{Y, B}) = \rho^{X, f^* B}
`$

拡張包括構造と射影分解

分裂ディスプレイクラス付き圏 $`(\cat{C}, \MC{D})`$ 上に、$`\cat{C}`$ のディスプレイ前層 $`\mrm{Disp}`$ を余域〈ターゲット前層〉とする自然変換 $`\rho`$ があるとします。このとき、$`(\cat{C}, \MC{D}, \rho)`$ が（$`\cat{C}`$ 上の）拡張包括構造〈extension-comprehension structure〉を定義します。

自然変換 $`\rho`$ の域〈ソース前層〉をステップ前層〈step presheaf〉と呼び、自然変換 $`\rho`$ は拡張自然変換〈extension natural transformation〉と呼びます。ここであらためて、ステップ前層は拡張包括構造の構成素と位置付けます。

この形の拡張包括構造は、ジェイコブスの包括圏〈comprehension category〉の特殊な場合（ファイブレーションが離散の場合）と同値なのですが、幾分かわかりやすい気がします。

カートメル構造のときに倣って、拡張関係 $`\ILT`$ を次のように定義します。

$`\quad X \ILT X' :\Iff \exists A\in \mrm{Step}(X).\, X' = X\cdot A`$

拡張包括構造を備えた圏 $`\cat{C}`$ において、$`Y \ILT Y'`$ である $`Y, Y'`$ に対して、次の射 $`g`$ を考えます。

$`\quad \xymatrix{
{}
& Y' \ar[d]^{\rho^{Y'}_Y}
\\
X \ar[ru]^g
& Y
}\\
\quad \In \cat{C}
`$

「最近の型理論： 拡張包括構造を持ったインデックス付き圏」では、この形の射をハープーン射と呼びました（設定は少し違いますが）。$`\cat{C}`$ がカートメル構造を持っていれば、任意の射がハープーン射になります。

上記の射 $`g`$ を、次の $`f, h`$ に分解したいと思います。以下で $`X \ILT X'`$ です。

$`\quad \xymatrix{
X' \ar[r]^{f^\uparrow} \ar@{.>}@/_1pc/[d]_{\rho^{X'}_X}
& Y' \ar[d]^{\rho^{Y'}_Y}
\\
X \ar[ru]^g \ar[r]_f \ar[u]_{h}
& Y
}\\
\quad \In \cat{C}
`$

ここで、実線で描かれた射達は可換になります。$`f^\uparrow`$ は、対象の拡張 $`Y\ILT Y', X\ILT X'`$ に伴う射の拡張〈持ち上げ〉 $`f \ILT f^\uparrow`$ です。$`h`$ は標準射影であるディスプレイ射 $`\rho^{X'}_X`$ のセクションになっています。つまり、次の等式が成立します。

$`\quad h ; \rho^{X'}_X = \id_X \;\In \cat{C}`$

このような分解が得られたとき、$`f`$ を $`g`$ の第一射影〈first projection〉、$`h`$ を第二射影〈second projection〉と呼びます。第一射影と第二射影から、もとの $`g`$ は $`h; f^\uparrow`$ として再現できます（[追記]「第一射影」「第二射影」は紛らわしい用語なので注意！ 「型理論に出てくる第一射影と第二射影」参照[/追記]）。

$`g`$ の第一射影は $`f := g; \rho^{Y'}_Y`$ とすればいいので簡単です。第二射影は、四角形がプルバック四角形であることから得られます。次の形の図式を考えます。

$`\quad \xymatrix@R+1pc@C+1pc{
X \ar@/^/[rrd]^g \ar@{=}@/_1pc/[rdd]_{\id_X} \ar@{.>}[dr]|{?}
&{}
&{}
\\
{}
& X' \ar[r]^{f^\uparrow} \ar[d]_{\rho^{X'}_X}
\ar@{}[dr]|{\text{p.b.} }
& Y' \ar[d]^{\rho^{Y'}_Y}
\\
{}
& X \ar[r]_f
& Y
}\\
\quad \In \cat{C}
`$

四角形がプルバックであることから、疑問符の射は一意に存在します。これを $`h:X \to X'`$ とします。次の等式は自動的に満たされます。

$`\quad g = h; f^\uparrow\\
\quad h; \rho^{X'}_X = \id_X
`$

$`h`$ が、目的の第二射影です。

型理論的解釈

拡張包括構造を備えた圏 $`\cat{C}`$ は、型理論的な圏となります。$`\cat{C}`$ は、型システムの構文論的構造をモデル化していると解釈できます。次のように解釈します。

• 圏 $`\cat{C}`$ の対象はコンテキスト〈context〉と解釈する。
• 圏 $`\cat{C}`$ の射は代入〈substitution〉と解釈する。
• 対象の拡張 $`(X, A) \mapsto X\cdot A`$ は、コンテキストに型宣言をひとつ追加することによるコンテキスト拡張〈context extension〉と解釈する。
• 標準射影 $`\rho^{X'}_X`$ は、新たに追加された型宣言は無視して、残りは自明な（恒等な）代入と解釈する。
• ステップ集合 $`\mrm{Step}(X)`$ の要素は、コンテキスト $`X`$ において整形式〈well-formed〉な型項〈type term〉と解釈する。
• セクションの集合 $`\mrm{Sect}(\rho^{X'}_X)`$ の要素は、コンテキスト $`X`$ において整形式〈well-formed〉なインスタンス項〈instance term〉と解釈する
• å°„ $`g:X \to Y' \:\text{ where }Y\ILT Y'`$ の射影分解は、代入の分解〈decomposition of substitution〉と解釈する。第一射影は拡張前の代入、第二射影は拡張した“差分”を表現するインスタンス項と解釈する。
• $`f^*, f^\#`$ の適用は、代入の型項／コンテキストへの適用〈application〉と解釈する。プレ結合引き戻し $`f^*`$ （記法はオーバーロードしている）は、インスタンス項への適用と解釈する。

呼び名の印象が違うので、奇妙な対応のように思えるかも知れませんが、呼び名を気にしなければ、構造的にはまっとうな対応です。

カートメル構造との比較

圏 $`\cat{C}`$ にカートメル構造 $`({\bf 1}, \ell, \mrm{ft}, \ILT)`$ が載っているとします。カートメル構造は拡張包括構造を定義しますが、単なる拡張包括構造より強い性質を持ちます。

カートメル構造では、「この世の始まりは何もなかった」という神話が事実になります。終対象 $`{\bf 1}`$ が「この世の始まり」「何もない状態」「空リスト」を表します。対象の長さ $`\ell`$ と親関数 $`\mrm{ft}`$ があることから次が言えます。

• 終対象以外のすべての対象は、有限回の拡張ステップにより作られたもの。その作り方は一意的である。

このことを説明しましょう。そのために、拡張関係 $`\ILT`$ の逆向きの記号（意味は同じ）を導入しておきます。

$`\quad Y \IGT X :\Iff X \ILT Y \Iff \mrm{ft}(Y) = X`$

終対象ではない任意の対象 $`X\in |\cat{C}|`$ をとると、次のような対象の系列が作れます。

$`\quad X \IGT X_1 \IGT \cdots \IGT X_n = {\bf 1}`$

ここで、$`n = \ell(X)`$ です。これは、$`|\cat{D}|`$ 上の関係 $`\IGT`$ が整礎〈well-founded〉である、ということです。終対象（世界の始まり）に至る系図を確実に有限的に辿れるので、正体不明の対象は存在しません。

対象の長さ $`\ell(X)`$ は、リストの長さ／ツリーのノードの高さとして解釈できますが、世界の始まりから勘定した世代〈generation〉の番号とも解釈できます。例えば、$`\ell(X) = 1`$ ならば、何もなかった世界に初めて生まれた第一世代の対象です。

カートメル構造では、明示的なステップ（型理論で言えば型）は存在しません。しかし、$`X \ILT X'`$ であるペア $`(X, X')`$ をステップと考えることができます。次の系列を考えてみます。

$`\quad {\bf 1} \ILT X_1 \ILT \cdots \ILT X_{n - 1} \ILT X_n = X`$

$`A_k := (X_{k - 1}, X_k)`$ と置くと、上記の列はステップのリストとして書けます。

$`\quad X = \langle A_1, \cdots, A_n\rangle`$

次々と拡張される系列は、仮想的“差分”であるステップのリストとして書けることになります。

カートメル構造を持つ圏は、長さ有限な、完全に正体が分かったステップのリストを対象（型理論で言えばコンテキスト）とするので、具体的な扱いが可能となります。