コンテキストの圏と指標の圏と限量子

「指標の圏はコンテキストの圏の反対圏」と「指標の圏に対する余ディスプレイ包含構造」で述べたように、コンテキストの圏と指標の圏は互いに反対圏です。この事実を利用することにより、型理論とインスティチューション理論を密接に結びつけることができます。

また、ローヴェア流の限量子の定式化をコンテキストの圏（指標の圏でもある）に組み込むことができます。このとき、コンテキストの圏の構造の一部は、ハイパードクトリンとしての役割りを持ちます。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
%\newcommand{\ot}{\leftarrow}
\newcommand{\op}{\mathrm{op}}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\Imp}{\Rightarrow }
\newcommand{\F}[1]{\mathscr{#1}} % remarkable functor
`$

内容：

全体の構造

型理論で出てくるコンテキストの圏（コンテキストを対象とする圏）と、インスティチューション理論で出てくる指標の圏（指標を対象とする圏）は互いに反対圏になっています。そのことは過去記事「指標の圏はコンテキストの圏の反対圏」に書いています。

コンテキストの圏を $`\cat{C}`$ 、指標の圏を $`\cat{S}`$ とします。すると：

$`\quad \cat{S} = \cat{C}^\op\\
\quad \cat{C} = \cat{S}^\op
`$

コンテキストの圏と指標の圏は表裏一体です。どちらが表か裏かは決められませんが、コンテキストの圏 $`\cat{C}`$ を表とするなら、指標の圏 $`\cat{S}`$ は“$`\cat{C}`$ を裏から見たもの”です。指標の圏 $`\cat{S}`$ を表とするなら、コンテキストの圏 $`\cat{C}`$ は“$`\cat{S}`$ を裏から見たもの”です。

カートメル／ヴォエヴォドスキー／パルムグレンの型理論（「 カートメル／ヴォエヴォドスキー／パルムグレンの型理論」参照）を採用するなら、コンテキストの圏 $`\cat{C}`$ は拡張包括構造とカートメルツリー構造（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）を持ちます。

一方、インスティチューション理論では、指標の圏 $`\cat{S}`$ に包含構造〈inclusion structure〉を載せることがよくあります（「指標の圏に対する余ディスプレイ包含構造」参照）。

$`\cat{C}`$ と $`\cat{S}`$ は一体なのですから、$`\cat{C}`$ 上の構造は $`\cat{S}`$ 上にも存在します。$`\cat{S}`$ 上の構造は $`\cat{C}`$ 上にも存在します。2つの圏が“一体化した単一の複合物”の上に構造が載っている、と考えることが重要です。

コンテキスト／指標の圏

2つの圏が一体化した単一の複合物をコンテキスト／指標の圏〈category of contexts/signatures〉と呼ぶことにします。コンテキスト／指標の圏には次の構造が載っています。

コンテキストの圏	指標の圏
特定された終対象	特定された始対象
ディスプレイクラス	余ディスプレイクラス
包括構é€	余包括構é€
標準プルバック四角形	標準プッシュアウト四角形
余域ファイブレーション	域反ファイブレーション
拡張構é€	拡張構é€
標準射影	標準入射
余包含構é€	包含構é€
カートメルツリー構é€	カートメルツリー構é€

1. 特定された終対象と特定された始対象は同一の対象で、空コンテキスト／空指標。
2. ディスプレイクラスは、ファイバー引き戻しに関して閉じた射の集合（「拡張包括構造のもうひとつの定式化〉参照）。同じ集合が、反対圏では余ファイバー押し出しに関して閉じた集合（余ディスプレイクラス）。
3. 包括構造は、ディスプレイ射と任意の射のコスパンにひとつの標準プルバック四角形を対応させる関手。アロー圏 $`\mrm{Arr}(\cat{C})`$ の余域関手が作る余域ファイブレーションの分裂子〈splitting〉になっている。余包含構造は、余ディスプレイ射と任意の射のスパンにひとつの標準プッシュアウト四角形を対応させる関手。アロー圏 $`\mrm{Arr}(\cat{C})`$ の域関手が作る域反ファイブレーションの分裂子になっている。
4. 拡張構造は、圏 $`\cat{C}`$ 上の前層と拡張演算の組み合わせで、拡張に伴う標準射影は包括構造と協調する。反対圏 $`\cat{S}`$ 上の拡張構造は、圏 $`\cat{S}`$ 上の余前層と拡張演算の組み合わせで、拡張に伴う標準入射は余包括構造と協調する。「拡張包括構造」、「拡張余包括構造」という言葉を使う都合で、どちらも（双対だが）拡張構造と呼ぶ。
5. 包含構造は、余ディスプレイクラスに関する制約で、広くやせた骨格的部分圏を形成することを要求する。余包含構造は、ディスプレイクラスに関する制約で、同じく、広くやせた骨格的部分圏を形成することを要求する。
6. カートメルツリー構造は、圏の対象の集合にツリー構造を与える。$`\cat{C}`$ と $`\cat{S}`$ で、ルートが終対象か始対象かの違いがあるが、それ以外の違いはないので、どちらも（双対だが）カートメルツリー構造と呼ぶ。

コンテキストの圏 $`\cat{C}`$ において、余包含構造を除いた構造達は、C-システム〈C-system〉の構造となります。余包含構造を含めると余包含的C-システム〈coinclusive C-system〉と言えるでしょう。指標の圏 $`\cat{S}`$ はその反対圏で、双対的な構造が載るので、包含的余C-システム〈inclusive co-C-system〉と言えます。

余包含構造／包含構造を要求すると、議論が極端に単純化されます。コンテキストの圏の余包含構造を使うことはほとんどないのですが、指標の圏の包含構造はよく使います。特に使う予定がなくても、反対圏の構造は嫌でも備わってしまいます（表裏一体なので）。

余包含的C-システム（同じことだが包含的余C-システム）は非常に強い構造です。が、構文的・具体的に定義されたコンテキストの圏（同じことだが指標の圏）は余包含的C-システムになります。

余包含的C-システムでは、2つの対象のあいだに余包含があれば、それはディスプレイ射で、ディスプレイ射は必ず余包含〈余包含射〉です。したがって、余包含とディスプレイ射を区別する必要はありません。余包含は依存射影〈dependent projection〉とも呼ばれます。標準射影〈canonical projection〉は、コンテキスト拡張〈context extension〉により誘導される依存射影です。すべての依存射影〈余包含〉が標準射影とは限りませんが、任意の依存射影〈ディスプレイ射 | 余包含射〉は幾つかの標準射影の結合として書けます。

上記の特徴は余包含的だからで、一般のC-システムで成立するわけではないので注意してください。

エス関手

コンテキスト／指標の圏を $`\cat{C}\& \cat{S}`$ とします。$`\cat{C}`$ と $`\cat{S}`$ は互いに反対圏で、$`\cat{C}`$ は余包含的C-システムである状況を考えます。

C-システムは（定義から）拡張包括構造を持ちます。$`\F{S}:\cat{C}^\op \to \mbf{Set}`$ （$`\F{S}`$ は筆記体のエス）は、拡張包括構造の一部である関手（前層）だとします。対象 $`\Gamma \in |\cat{C}|`$ ごとに、次のような拡張関数があります。

$`\quad \mrm{Ext}_\Gamma : \F{S}(\Gamma) \to |\cat{C}|`$

下付きの $`\Gamma`$ に渡って寄せ集めると、$`\mrm{Ext}`$ の総体が定義できます。

$`\quad \mrm{Ext} \in \prod_{\Gamma \in |\cat{C}|} \mrm{Map}( \F{S}(\Gamma), |\cat{C}|)`$

これは次のようにも書けます。

$`\quad \mrm{Ext} : (\sum_{\Gamma\in |\cat{C}|} \F{S}(\Gamma)) \to |\cat{C}| \In \mbf{SET}
`$

依存ペア $`(\Gamma, A) \in \sum_{\Gamma\in |\cat{C}|} \F{S}(\Gamma)`$ に対する拡張の値は、中置演算子記号 '$`\cdot`$' を用いて $`\Gamma\cdot A`$ と書きます。

$`\text{For }\Gamma \in |\cat{C}|, A\in \F{S}(\Gamma)\\
\quad \Gamma \cdot A := \mrm{Ext}(\Gamma, A) = \mrm{Ext}_{\Gamma}(A)
`$

型理論の文脈では、$`\F{S}(\Gamma)`$ の要素は「コンテキスト $`\Gamma`$ で許容できる型項」と考えます。型項は実際は型ファミリー項*1で、$`\Gamma`$ がファミリーのパラメータ領域を与えます。

一方、インスティチューション理論では、$`\F{S}(\Gamma)`$ の要素は「指標 $`\Gamma`$ に追加できる論理文」と考えます。論理文〈logical sentence〉、あるいは単に文〈sentence〉とは、閉じた論理式（自由変数を持たない論理式）と同じことです。文とは、指標 $`\Sigma`$ に対して意味を持つ命題ともいえます。

型項と文では全然違うものに思えますが、カリー／ハワード／ランベック対応によれば「型と命題は同じもの」です。曖昧語「型」は型項と解釈できるし、曖昧語「命題」は文〈論理式〉と解釈できる（「命題」と「型」の曖昧性を図示」参照）ので、型項と文が同じものであることは、さほど驚くことではありません。

$`\F{S}`$ はコンテキストの圏 $`\cat{C}`$ 上の反変関手〈前層〉ですが、指標の圏 $`\cat{S}`$ 上では共変関手〈余前層〉です。コンテキスト／指標の圏 $`\cat{C}\& \cat{S}`$ 上で定義された関手 $`\F{S}`$ をエス関手〈ess functor〉と呼ぶことにします。'S' は次に由来します。

1. 型理論におけるソート〈sort〉。ソートと型は同義語。
2. インスティチューション理論における文〈sentence〉。文と命題は同義語。
3. 拡張におけるステップ〈step〉（「拡張包括構造のもうひとつの定式化」参照）。

構文的・具体的に定義された指標 $`\Gamma`$ （「実用になる型理論の記法」参照）においては、$`\F{S}(\Gamma)`$ は指標に追加可能な宣言文の集合とみなせます。ソート〈型〉やオペレーション〈関数〉を導入する宣言文の場合もあれば、法則の宣言文〈公理の命題〉の場合もあります。

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

一般的に、圏の射 $`f:A \to B`$ に対して、$`f`$ のセクション〈section〉 $`s`$ 、$`f`$ のレトラクション〈retraction | リトラクション〉 $`r`$ とは次を満たす射です。

• セクション条件： $`s:B\to A,\; s;f = \id_B`$
• レトラクション条件： $`r:B\to A,\; f;r = \id_A`$

任意の射にセクションやレトラクションが存在するわけではありません -- 例えば、集合圏で考えてみてください。セクションは、反対圏ではレトラクションになります。コンテキストの圏のセクションは指標の圏のレトラクションになります。

コンテキスト（指標と言っても同じ）$`\Gamma`$ と $`A\in \F{S}(\Gamma)`$ に対して、コンテキスト拡張 $`\Gamma\cdot A`$ と標準射影 $`\rho^{\Gamma, A}`$ が決まります。

$`\quad \rho^{\Gamma, A} : \Gamma\cdot A \to \Gamma \In \cat{C}`$

標準射影（反対圏では標準入射） $`\rho^{\Gamma, A}`$ のセクション（反対圏ではレトラクション）は重要です。通常、型理論で「インスタンス」と言った場合、標準射影のセクションを指すことが多いです。が、「インスタンス」は曖昧多義語なので、セクションインスタンス〈section instance〉と呼んだほうが紛れがないでしょう。その他の「インスタンス」の用法については「型理論のインスタンスとは」を見てください。

型理論では、構文論と意味論をあまり区別しない（あるいは区別し難い）ので、構文論的なセクションインスタンス項と意味論的なセクションインスタンス実体をともに「項」と呼ぶことが多いです（語尾の「項」「実体」は「「命題」と「型」の曖昧性を図示」参照）。この略語はだいぶ理不尽ですが多数派です。論理で“項”に対応するのは定理の証明です。このことは、Proofs-as-Terms, Terms-as-Proofs というキャッチフレーズで表現されます（「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」参照）。

標準射影のセクション全体の集合は、次のように書きます。

$`\quad \mrm{Sect}(\rho^{\Gamma, A}) = \mrm{Sect}(\rho^{\Gamma, A}: \Gamma\cdot A \to \Gamma)`$

標準射影のセクションやセクション達の集合には様々な呼び名があります。が、今それらを列挙するのは意味がないと思うのでしません。ひとつだけ注意しておくと、$`s\in \mrm{Setc}(\rho^{\Gamma, A})`$ であることを、型理論の標準的記法では次のように書きます。

$`\quad \Gamma \vdash s : A`$

上記の構文形式〈syntactic form〉は型判断〈{type | typing} judgement〉と呼びます。

標準射影のセクション $`\rho^{\Gamma, A}`$ の反対圏における対応物（向きを逆にしただけ）を $`\tau^{\Gamma, A}`$ とします。

$`\quad \tau^{\Gamma, A} : \Gamma \to \Gamma \cdot A \In \cat{S}`$

$`\tau^{\Gamma, A}`$ は指標の圏 $`\cat{S}`$ の標準入射〈canonical injection〉です。$`\cat{S}`$ は包含的〈inclusive〉と仮定していたので、標準入射は包含〈包含射〉であり、余ディスプレイ射でもあります。

標準入射のレトラクション全体の集合は、次のように書きます。

$`\quad \mrm{Retr}(\tau^{\Gamma, A}) = \mrm{Retr}(\tau^{\Gamma, A}: \Gamma \to \Gamma\cdot A)`$

ここで、同じ概念に呼び名（同義語）がバカみたいに増える事情に触れておきます。コンテキストの圏 $`\cat{C}`$ に関するなんらかの概念があったとき：

1. 型理論の文脈で、構文論的観点から $`\cat{C}`$ 上の概念に名前を付ける。
2. 型理論の文脈で、意味論的観点から $`\cat{C}`$ 上の概念に名前を付ける。
3. 論理の文脈で、構文論的観点から $`\cat{C}`$ 上の概念に名前を付ける。
4. 論理の文脈で、意味論的観点から $`\cat{C}`$ 上の概念に名前を付ける。
5. 型理論の文脈で、構文論的観点から 反対圏 $`\cat{S}`$ 上の概念に名前を付ける。
6. 型理論の文脈で、意味論的観点から 反対圏 $`\cat{S}`$ 上の概念に名前を付ける。
7. 論理の文脈で、構文論的観点から 反対圏 $`\cat{S}`$ 上の概念に名前を付ける。
8. 論理の文脈で、意味論的観点から 反対圏 $`\cat{S}`$ 上の概念に名前を付ける。

しかも、ネーミングルールが統制されているわけではないので、結果としてグチャグチャになります。

エス関手とハイパードクトリン

コンテキスト／指標の圏 $`\cat{C}\& \cat{S}`$ のエス関手 $`\F{S}`$ は次のような関手でした。

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

あるいは（同じことですが）：

$`\quad \F{S} : \cat{S} \to \mbf{Set} \In \mbf{CAT}`$

エス関手の余域を、集合圏 $`\mbf{Set}`$ から順序集合の圏 $`\mbf{Ord}`$ に変更します。

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

こう変更すると、$`\F{S}(\Gamma)`$ は単なる集合ではなくて順序関係 $`\le`$ を持ちます。型理論で言えばサブタイプ関係、論理で言えばエンテイルメント関係です -- これは典型例で、別にどんな順序関係でもかまいませんけどね。

$`\varphi`$ が圏 $`\cat{C}`$ の依存射影〈ディスプレイ射〉（標準射影でなくてもよい）のとき、$`\F{S}(\varphi)`$ を水増し〈thinning〉と呼びます。定義から、水増しは圏 $`\mbf{Ord}`$ の射です。「水増し」は、論理における「論理式／述語の変数水増し」に対応するからで、他の文脈・観点からは別な名前が付いています（前節の最後参照）。

標準射影 $`\rho^{\Gamma, A}`$ は依存射影の特別なものなので、$`\F{S}(\rho^{\Gamma, A})`$ は水増しです。余包含的なコンテキストの圏では、一般の依存射影は標準射影の結合で書けるので、標準射影の水増しを考えれば十分です。標準射影の水増しを次のように書きます。

$`\quad \Delta_{\Gamma, A} := \F{S}(\rho^{\Gamma, A})\\
\quad \Delta_{\Gamma, A} : \F{S}(\Gamma)\to\F{S}(\Gamma \cdot A) \In \mbf{Ord}
`$

習慣的に $`\Delta`$ を使うのは、水増しの非常に特別な場合が対角写像になるからです。僕の過去記事では、$`\Delta`$ の代わりに $`\diamondsuit`$ を使ったこともあります。

水増しは依存射影、つまりディスプレイ射（ディスプレイクラスの要素）に対してしか定義しません。というか、ディスプレイ射に対するエス関手の値（圏 $`\mbf{Ord}`$ の射）を水増しと定義したのでした。ディスプレイ射達は、“ファイバー引き戻しに関して閉じている”という良い性質を持っていました。

$`\mbf{Ord}`$ に値をとるエス関手を備えたコンテキスト／指標の圏は、ローヴェアのハイパードクトリンのセットアップ〈準備的な状況設定〉となります。エス関手と標準射影が次の条件を満たすとき、圏 $`\cat{C}`$ 上のハイパードクトリン〈hyperdoctrine〉となります。

• 任意の標準射影 $`\rho^{\Gamma, A}`$ に対して、水増し $`\Delta_{\Gamma, A}`$ は左随伴と右随伴を持つ。

左随伴／右随伴は圏論の意味の随伴ですが、順序集合の圏ではガロア接続ということもあります（「順序随伴性： ガロア接続の圏論」参照）。

今扱っているコンテキストの圏は余包含的C-システムなので、任意の射影〈依存射影〉は標準射影の結合で書けます。よって、ハイパードクトリンの条件を次のように言っても同じです。

• 任意の射影〈ディスプレイ射〉の水増しは左随伴と右随伴を持つ。

いっとき、ハイパードクトリンの定義を二重圏ベースで出来ないか？ と考えていたのですが（以下の過去記事参照）、C-システムのエス関手に条件を付けたほうが具合がいいような気がします。

• 述語論理： 二重圏的ハイパードクトリン
• 述語論理： シード付き二重圏 -- 訂正と再論

過去記事でシード射と呼んでいた射が射影〈ディスプレイ射〉で、シード四角形と呼んでいた四角形が射影に伴うプルバック四角形です。

外部シグマ・パイと内部シグマ・パイ

コンテキスト拡張 $`\Gamma\cdot A`$ を $`\sum_\Gamma A`$ と書くことがあります。セクション達の集合 $`\mrm{Setc}(\rho^{\Gamma, A})`$ を $`\prod_\Gamma A`$ と書くことがあります。これは、コンテキストの圏の特殊ケースとして集合圏を考えたときに、コンテキスト拡張がシグマ型に、セクション達の集合がパイ型となっているからです。

一方で、エス関手がハイパードクトリンを定義するとき、水増し関手 $`\Delta_{\Gamma, A}`$ の左随伴を $`\Sigma_{\Gamma, A}`$ 、右随伴を $`\Pi_{\Gamma, A}`$ と書いたりもします。$`\Sigma, \Delta, \Pi`$ が作る随伴トリプルをΣ-Δ-Π随伴〈Σ-Δ-Π adjunction〉と呼んだりします。この随伴トリプルは、エス関手の性質として定義されます。

最初のシグマ・パイは、コンテキストの圏の拡張包括構造から出てくるものです。二番目のシグマ・パイは、エス関手によるハイパードクトリンのなかの概念です。特別な例では、二種類のシグマ・パイが一致することもあるのですが、区別しておくのが吉です。一番目の意味のシグマ・パイを外部シグマ・パイ〈external sigma-pi〉、二番目の意味のシグマ・パイを内部シグマ・パイ〈internal sigma-pi〉と呼び分けましょう。

もし、論理の文脈で語っているなら、外部シグマ・パイはデータ型の集合論的シグマ型とパイ型と解釈できて、内部シグマは存在限量子〈existential quantifier〉、内部パイは全称限量子〈universal quantifier〉になります。この場合は、外部シグマ・パイと内部シグマ・パイは別物なので混同することはありませんが、一般的な状況だと混同しがちなので注意してください。

そしてそれから

エス関手を使ったハイパードクトリンの定義はすぐに拡張できます。エス関手の余域を圏達の圏にして、ガロア接続〈順序随伴〉を圏論の随伴に変えれば、圏を論理代数（「述語論理： ベース圏と論理代数の圏」参照）とするハイパードクトリンを作れます。

論理代数として、単なる圏より演繹系（ある種のオペラッド）のほうが現実的かも知れません。π-インスティチューションの概念（以下の過去記事参照）を、コンテキスト／指標の圏の上で再定義できそうです。

• 演繹系と閉包系
• ダラッっと依存型理論・インスティチューション

アブラムスキー達の仕様構造（「ホーア論理の圏論的な定式化」参照）も、コンテキスト／指標の圏に取り込めるかも知れません。

この記事では、指標にモデル圏を対応させる関手についてはまったく触れてません。インスティチューション理論の主役はモデルのほうです。指標の圏が、構文モナドのクライスリ圏であることも、この記事では触れてません。

コンテキスト／指標の圏 $`\cat{C}\& \cat{S}`$ は、様々な話題に関連する豊富な構造達をホストする良い土台になりそうです。

*1:型ファミリー項も単に「型項」、さらには単に「型」と呼ぶ習慣があるのです。