インスティチューション理論の骨組みに、型理論やモナドを使って肉付けしようという目論見（「構文付き変換手インスティチューション 1/n」における“半具象インスティチューション”）は、型理論的圏の反対圏が指標の圏として使えることが分かってちょっと進捗しました（「型理論とインスティチューション理論が繋がるぞ！」参照）。このタイミングで、型理論的圏について再確認しておきます。
型理論的圏 -- つまり型理論／型システムの圏論的モデル*1は、色々と提案されています。カートメルのコンテキスト圏〈contextual category〉は、そのなかでも具体的で扱いやすいものです。ヴォエヴォドスキーは、コンテキスト圏をC-システムと再命名しました。ここでは、C-システム〈コンテキスト圏〉を、ニ種類の構造のハイブリッドとして定義してみます。$`\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
`$
内容：
C-システム
ヴォエヴォドスキー〈Vladimir Voevodsky〉は、型理論の理論〈theory of type theories〉の基礎としてカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉を採用しました。が、呼び名はC-システム〈C-system〉に変更しています。「コンテキスト圏」と呼びたくない理由は次の論文の冒頭に書いてあります。
- [Voe14-16]
- Title: Subsystems and regular quotients of C-systems
- Author: Vladimir Voevodsky
- Submitted: 28 Jun 2014 (v1), 15 Mar 2016 (v3)
- Pages: 12p
- URL: https://arxiv.org/abs/1406.7413
事情はともかく、「カートメルのC」と「コンテキストのC」からC-システムだと憶えておけばいいでしょう。
C-システムは、次のような複数の構造と性質に分けて理解すると良いと思います。
- 圏の上の分裂ディスプレイクラス
- 同じ圏の上のカートメルツリー構造
- 分裂ディスプレイクラスとカートメルツリー構造が協調することを表す標準プルバック四角形公理
分裂ディスプレイクラス
分裂ディスプレイクラスについて「拡張包括構造のもうひとつの定式化」で述べました。形容詞「分裂〈split〉」は特定の分裂子〈splitting〉が指定されていること、つまり分裂子付き〈with splittng〉の意味で使います（「ファイブレーションの亀裂と分裂」参照）。したがって、分裂ディスプレイクラス付き圏〈category with split display class〉は次のように書くのが正確です。
$`\quad (\cat{C}, \MC{D}, \mrm{Spl})`$
ここで、$`\mrm{Spl}`$ は特定された分裂子です。分裂子〈splitting〉をきちんと定義しておきましょう。まず、圏 $`\cat{C}`$ の射のクラス（「射のクラスと制約付きスパン // 圏の射のクラス」参照） $`\MC{A}, \MC{B} \subseteq \mrm{Mor}(\cat{C})`$ に相対的なコスパン達の集合を定義します。
$`\quad \mrm{Cosp}_\cat{C}( \MC{A}, \MC{B}) := \\
\qquad \{
(f, g)\in \mrm{Mor}(\cat{C})^2 \mid
f \in \MC{A}, g\in \MC{B}, \mrm{cod}(f) = \mrm{cod}(g)
\}`$
写像 $`\mrm{Spl}`$ の域〈ドメイン〉は、集合 $`\mrm{Cosp}_\cat{C}(\mrm{Mor}(\cat{C}), \MC{D})`$ です。つまり、左余脚〈left coleg〉は任意の射で右余脚〈right coleg〉はディスプレイ射（クラス $`\MC{D}`$ の要素）であるコスパン達の集合です。
$`\cat{C}`$ のプルバック四角形、つまりコスパンの極限錐となる可換四角形*2をすべて寄せ集めた集合を $`\mrm{PBSq}(\cat{C})`$ とします。可換四角形の各部を次の名前で呼ぶことにします。
$`\quad \xymatrix{
\mrm{TopLeft} \ar[r]^{\mrm{top}} \ar[d]_{\mrm{left}}
& \mrm{TopRight} \ar[d]^{\mrm{right}}
\\
\mrm{BottomLeft} \ar[r]_{\mrm{bottom}}
& \mrm{BottomRight}
}`$
可換四角形の各部を取り出す関数も同じ名前とします。なお、圏 $`\cat{C}`$ は小さいとしています。
$`\quad
\mrm{top},\mrm{left},\mrm{right},\mrm{bottom} : \mrm{PBSq}(\cat{C}) \to \mrm{Mor}(\cat{C}) \In {\bf Set}\\
\quad
\mrm{TopLeft},\mrm{TopRight},\mrm{BottomLeft},\mrm{BottomRight} : \\
\qquad \mrm{PBSq}(\cat{C}) \to \mrm{Obj}(\cat{C}) \In {\bf Set}
`$
$`\mrm{Spl}`$ は次のような関数です。
$`\quad \mrm{Spl} : \mrm{Cosp}_\cat{C}( \mrm{Mor}(\cat{C}), \MC{D}) \to \mrm{PBSq}(\cat{C})
\In {\bf Set}
`$
$`\mrm{Spl}(f, d)`$ の $`\mrm{bottom}`$ は $`f`$ で $`\mrm{right}`$ は $`d`$ になるので、以下の可換図式があります。以下で $`\mrm{first}, \mrm{second}`$ は直積の第一／第二射影です。
$`\quad \xymatrix{
\mrm{Cosp}_\cat{C}( \mrm{Mor}(\cat{C}), \MC{D})
\ar[r]^-{\mrm{Spl}} \ar[d]_{\mrm{first}}
& \mrm{PBSq}(\cat{C}) \ar[d]^{\mrm{bottom}}
\\
\mrm{Mor}(\cat{C}) \ar@{=}[r]
& \mrm{Mor}(\cat{C})
}\\
\quad \text{commutative }\In {\bf Set}
`$
$`\quad \xymatrix{
\mrm{Cosp}_\cat{C}( \mrm{Mor}(\cat{C}), \MC{D})
\ar[r]^-{\mrm{Spl}} \ar[d]_{\mrm{second}}
& \mrm{PBSq}(\cat{C}) \ar[d]^{\mrm{right}}
\\
\mrm{Mor}(\cat{C}) \ar@{=}[r]
& \mrm{Mor}(\cat{C})
}\\
\quad \text{commutative }\In {\bf Set}
`$
コスパン $`(f, d)`$ のプルバック四角形に対して、次のように記法の約束をします*3。
$`\quad f^\# \mrm{dom}(d) := \mrm{TopLeft}(\mrm{Spl}(f, d))\\
\quad f^\# d := \mrm{left}(\mrm{Spl}(f, d))\\
\quad f \uparrow d := \mrm{top}(\mrm{Spl}(f, d))
`$
$`\quad \xymatrix{
{f^\#\mrm{dom}(d)} \ar[r]^{f \uparrow d} \ar[d]_{f^\# d}
\ar@{}[dr]|{\text{p.b.}}
& \mrm{dom}(d) \ar[d]^d
\\
\cdot \ar[r]_f
& \cdot
}\\
\quad \In \cat{C}
`$
この記法を使うと、$`\mrm{Spl}`$ が第一引数に関して反変関手的であることを次のように書けます。
$`\text{For } f: X\to Y,\, g:Y \to Z,\, d : W \to Z \; \in \cat{C}\\
\quad (f; g)^\# W = f^\# (g^\# W)\\
\quad {\id_Z}^\# W = W\\
\quad (f; g)^\# d = f^\# (g^\# d)\\
\quad {\id_Z}^\# d = d\\
\quad (f; g) \uparrow d = (f\uparrow ( g^\# d ) ) ; (g \uparrow d)\\
\quad \id_Z \uparrow d = \id_W
`$
$`\quad \xymatrix{
\cdot \ar[r] \ar[d]
\ar@{}[dr]|{\text{p.b}}
&\cdot \ar[r] \ar[d]
\ar@{}[dr]|{\text{p.b}}
& W \ar[d]^d
\\
X \ar[r]_f
& Y \ar[r]_g
& Z
}`$
分裂ディスプレイクラス付き圏 $`(\cat{C}, \MC{D}, \mrm{Spl})`$ とは、上記の法則（反変関手性）を満たすような $`\MC{D}, \mrm{Spl}`$ を備えた圏です。$`\MC{D}`$ をそのディスプレイクラス〈display class〉、$`\mrm{Spl}`$ をその分裂子〈splitting〉と呼びます。分裂子から誘導された反変関手が、「拡張包括構造のもうひとつの定式化 」で述べた $`\mrm{Disp}`$ です。
カートメルツリー構造
カートメル構造については「パルムグレンによる、型理論の複前層モデル // カートメル構造」で述べています。過去記事のカートメル構造は、分裂ディスプレイクラスの定義も含んでいて、C-システムの定義そのものです。ここでは、圏の対象の集合をツリー状に編成する部分だけをカートメルツリー構造〈Cartmell tree structure〉と呼ぶことにします。
圏 $`\cat{C}`$ 上のカートメルツリー構造は次の構成素からなります。
- 特定された終対象 $`{\bf 1} \in |\cat{C}|`$
- 長さ〈length〉関数 $`\ell : |\cat{C}| \to {\bf N}`$
- 親〈parent | father〉関数 $`\mrm{ft} : |\cat{C}|\setminus \{{\bf 1}\} \to {\bf N}`$
- 子から親に向かう射を与える関数 $`\rho^\hyp : |\cat{C}|\setminus \{{\bf 1}\} \to \mrm{Mor}(\cat{C})`$
法則は「パルムグレンによる、型理論の複前層モデル // カートメル構造」に書いてますが繰り返すと：
- $`\ell(X) = 0 \Iff X = {\bf 1}`$
- $`\ell(\mrm{ft}(X)) = \ell(X) - 1 \;\text{ where } X \ne {\bf 1}`$
- $`\mrm{dom}(\rho^X) = X \land \mrm{cod}(\rho^X) = \mrm{ft}(X) \;\text{ where } X \ne {\bf 1}`$
$`\rho^X`$ は（冗長ですが）$`\rho^X_{\mrm{ft}(X)}`$ とも書きます。拡張関係 $`\ILT`$ は親関数から定義できるのでカートメルツリー構造の定義には入っていません。拡張関係を使って書くほうが便利なこともあります。
カートメルツリー構造の定義は以上で終わりです。圏の対象をノードとするツリーを定義しているだけです。
分裂ディスプレイクラス ＋ カートメルツリー構造
圏 $`\cat{C}`$ 上に、分裂ディスプレイクラス $`\MC{D}, \mrm{Spl}`$ と、カートメルツリー構造 $`{\bf 1}, \mrm{ft}, \rho`$ が載っているとします。分裂ディスプレイクラスとカートメルツリー構造が協調するために、まず次の条件を課します。
- $`\forall X\in |\cat{C}|.\, \rho^X \in \MC{D}`$
$`Y \ILT Y'`$ （$`\mrm{ft}(Y') = Y`$）だとして、分裂子 $`\mrm{Spl}`$ によるプルバック四角形 $`\mrm{Spl}(f, \rho^{Y'})`$ を考えます。
$`\quad \xymatrix{
{f^\# Y'} \ar[r]^{f \uparrow \rho^{Y'}} \ar[d]_{f^\# \rho^{Y'}}
\ar@{}[dr]|{\text{p.b.}}
& Y' \ar[d]^{\rho^{Y'}}
\\
X \ar[r]_{f}
& Y
}\\
\quad \In \cat{C}`$
先の条件から $`\rho^{Y'} \in \MC{D}`$ なので、上記のプルバック四角形は（$`\mrm{Spl}`$ により）一意的に作れます。さらに次の条件を満たすことを要求します。
- $`X \ILT {f^\# Y'}`$
- $`{f^\# \rho^{Y'}} = \rho^{f^\# Y'}`$
この条件〈公理〉を標準プルバック四角形公理〈canonical pullback square axiom〉と呼ぶことにします。これは、分裂子が作るプルバック四角形の左右の射が、カートメルツリーの枝になっていることを主張しています。カートメルツリーの枝である射のクラスは、ファイバー引き戻しに関して閉じているのです。
圏の上に、分裂ディスプレイクラスとカートメルツリー構造が載っていて、標準プルバック四角形公理を満たすなら、それはC-システム〈C-system〉です。
