いろいろな概念をツギハギしてゴニョゴニョ・ガチャガチャしているうちに、表題のごとき事が分かりました。「あー、よかった」という気持ちでいます。内容的なことを詳しく書く気が起きないので、とりとめもなく雑感を記します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Longrightarrow} % for meta prop
%\newcommand{\hyp}{ \text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\Ent}{ \mathrel{|\!\!\!\Rightarrow} } % entail
`$
内容：
ν-インスティチューション
「ダラッっと依存型理論・インスティチューション // ν-インスティチューション」において、「ν-インスティチューション」〈nu-institution〉という言葉を出したんですが、それ以前に「半具象インスティチューション〈semi-concrete institution〉」と呼んでいたものに別名を与えただけです。「半具象インスティチューション」にハッキリした定義があるわけではないので、「ν-インスティチューション」もハッキリしない雰囲気的な概念です。
ν-インスティチューション（「ν」はブイじゃなくてニュー）がオリジナルのインスティチューションと違う点、目的とするところは：
- インスティチューションでは公理として与えられている構造や性質の一部を、より基本的な公理から構成・証明する。
- 依存型理論と統合する。
オリジナルのインスティチューション（ゴグエン／バーストル〈Joseph Goguen, Rod Burstall〉のインスティチューション）は、バーワイズ〈Jon Barwise〉の抽象モデル理論の圏論的定式化なので、そのスピリッツ〈精神・真髄〉は継承します。つまり、モデル理論を含む論理の定式化に使えるようにする、ということです。
依存型理論には、様々な定式化・流儀があります。インスティチューションと相性が良さそうなものを挙げると：
- ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉
- カートメル／ヴォエヴォドスキー〈John Cartmell, Vladimir Voevodsky〉のC-システム〈C-system〉（カートメルの用語ではコンテキスト圏〈contextual category〉）
- ジョイアル〈Andre Joyal〉のクラン〈clan〉
抽象度が高い鳥の視点〈bird's eye view〉で見るときは包括圏を利用します。より具体的な虫の視点〈Bug's eye view〉では、C-システムとクランを組み合わせた構造を使います。
現時点におけるν-インスティチューションは、次のようなものを想定しています。
- 台となる圏 $`\cat{C}`$ はクランである。
- クラン $`\cat{C}`$ 上にエス関手 $`\msc{S}`$ が載っている。
- エス関手 $`\msc{S}`$ に基づいた拡張包括構造が載っている。
クランと双対概念であるコクランについては次の過去記事に書いています。
エス関手 $`\msc{S}`$ については、次を参照してください。
拡張包括構造については次の過去記事に書いています。
クランには、「拡張包括構造のもうひとつの定式化」におけるディスプレイクラスより使いやすいファイブレーションクラスが備わっています。「コンテキストの圏と指標の圏と限量子 // エス関手」のエス関手とは、「拡張包括構造のもうひとつの定式化」におけるステップ前層のことだと思ってかまいません。
C-システムにはカートメルツリー構造（「C-システム、分裂ディスプレイクラス、カートメルツリー構造 // カートメルツリー構造」参照）が備わっていますが、ν-インスティチューションの定義としては不要なようです。必要になった時点でカートメルツリー構造を追加するでいいでしょう。
インスティチューション理論はモデル理論を継承しているので、モデル関手を持っています。クラン $`\cat{C}`$ 上で定義されたモデル関手（の一般化）を、ここではエム関手〈em functor〉と呼びます。エム関手は次のような関手です。
$`\quad \msc{M} : \cat{C} \to \cat{T} \In \mbf{CAT}`$
エム関手のターゲット圏〈余域圏〉のサイズが大きいときは、次のようになることがあります。（$`\mathbb{CAT}`$ はとても大きい圏達の2-圏。）
$`\quad \msc{M} : \cat{C} \to \cat{T} \In \mathbb{CAT}`$
ゴグエン／バーストルのインスティチューション（の再定式化）では、エム関手のターゲット圏は $`{_1\mrm{Cat}}`$ または $`{_1\mrm{CAT}}`$ です。右下付きの 1 は、2-射〈自然変換〉を捨てていることを示します。
エム関手には条件が付きます。無条件では、「型理論とインスティチューション理論が繋がるぞ！」の構成が出来ません。条件は、ある種の有限連続性です（後述）。
エム関手も入れると、ν-インスティチューションの構成素達は次のものです。
- クラン $`\cat{C}`$
- エス関手 $`\msc{S} : \cat{C}^\op \to \mbf{Set}`$
- 拡張包括構造 $`\mrm{CPBSq}`$
- エム関手 $`\msc{M} : \cat{C} \to \cat{T}`$
$`\mrm{CPBSq}`$ は Canonical PullBack Square のつもりで、標準射影のコスパンに標準プルバック四角形（より正確に言えば、標準プルバック極限錐）を対応させる写像で、幾つかの条件を満たすものです。
エム関手は依存型理論にはない概念です。伝統的モデル理論をやるのであれば、エム関手のターゲット圏は $`{_1\mbf{CAT}}`$ と置きます。ν-インスティチューションはいわば、エム関手を備えた依存型理論であり、述語論理とそのモデル理論を吸収できます。
包括圏とデカルト関手
ν-インスティチューションを鳥の視点で見るときは、包括圏として扱います。包括圏 $`\msc{K}`$ の構成素は次のものです。
- 全体圏〈total category〉 $`\mrm{Tot}(\msc{K}) \in |\mbf{CAT}|`$
- ベース圏〈base category〉 $`\mrm{Base}(\msc{K}) \in|\mbf{CAT}|`$
- 射影関手〈projection functor〉 $`\mrm{Proj}^\msc{K}:\mrm{Tot}(\msc{K})\to \mrm{Base}(\msc{K}) \In \mbf{CAT}`$
- 包括関手〈comprehension functor〉 $`\mrm{Comph}^\msc{K} : \mrm{Tot}(\msc{K})\to \mrm{Arr}(\cat{C})\In \mbf{CAT}`$
我々が扱うケースでは、ベース圏はクラン $`\cat{C}`$ の台圏です。記号を乱用して、クランとその台圏を同じ記号 $`\cat{C}`$ で表します。
記法を簡素化するために、全体圏を $`\cat{E}`$ 、射影関手を $`\pi`$ 、包括関手を $`\gamma`$ と書くことにします。包括圏の条件〈公理 | 法則〉を記述するために、以下の図式を使います。
$`\quad \xymatrix{
\cat{E} \ar[d]_\pi \ar[r]^\gamma
&{\mrm{Arr}(\cat{C})} \ar[d]^{\mrm{Cod}}
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\quad \In {_1 \mbf{CAT}}`$
$`\mrm{Arr}(\cat{C})`$ は、圏 $`\cat{C}`$ のアロー圏です（「アロー圏 ＝ バンドルの圏」参照）。「アロー圏」と「バンドルの圏」は同義語です。$`\vec{\mbf{2}}`$ を二元集合 $`\{0, 1\}`$ に恒等射2つと、非恒等射1つだけ $`0\to 1`$ を乗せた圏だとして、アロー圏は次の関手圏としても定義できます。
$`\quad \mrm{Arr}(\cat{C}) := [\vec{\mbf{2}}, \cat{C}] = \cat{C}^{\vec{\mbf{2}}}`$
関手圏としての定義において、関手 $`\mrm{Cod}`$ は、$`1\in |\vec{\mbf{2}}|`$ で関手／自然変換を評価〈evaluate〉する関手です。バンドルで言えば、バンドル／バンドル射のベースパートを取り出す関手です。
さて、包括圏の条件は：
- 上の図式は可換である。
- $`\pi : \cat{E} \to \cat{C}`$ は圏のファイブレーションである。
- $`\gamma : \cat{E} \to \mrm{Arr}(\cat{C})`$ はデカルト関手である。
「圏のファイブレーション」は「ファイバー付き圏〈fibered category〉」「グロタンディーク・ファイブレーション〈Grothendieck fibration〉」と同義語です。
「デカルト関手」は曖昧多義語で困るんですが、「集合のバンドルと圏のバンドル // デカルト関手とファイバー付き圏」で述べた意味でのデカルト関手です。古い記事「圏のファイブレーション」にも記述があります。
「ダラッっと依存型理論・インスティチューション」において、次のように書きました。
包括圏の定義は、初見では「なに言ってるんだ？」ですが、他の型理論的圏の定義をパッキングする（抽象的にまとめる）と確かに包括演算に帰着します。
包括圏は分かりにくいですが、良いニュースは、ここで使う包括圏はとても単純なものだけなことです。圏のファイブレーション〈グロタンディーク・ファイブレーション〉において、ファイバーがすべて（小さい）離散圏であるものを離散ファイブレーション〈discrete fibration〉といいます。ν-インスティチューションに対応する包括圏では、$`\pi : \cat{E} \to \cat{C}`$ は離散ファイブレーションです。
離散ファイブレーションは極端に単純なファイブレーションで、ベース圏（今の場合は $`\cat{C}`$）上の前層と一対一対応します。つまり、離散ファイブレーションと前層は同一視できます。今の場合は、エス関手 $`\msc{S}`$ と $`\pi : \cat{E} \to \cat{C}`$ が同一視できます。別な言い方をすると、$`\pi : \cat{E} \to \cat{C}`$ は $`\msc{S}`$ のグロタンディーク構成〈要素の圏〉とその標準射影です。
$`\quad \cat{E} = {\displaystyle \int_{\cat{C}} }\msc{S}`$
包括圏の包括関手 $`\gamma : \cat{E} \to \mrm{Arr}(\cat{C})`$ は、拡張包括構造の $`\mrm{CPBSq}`$ から構成できます。$`\mrm{CPBSq}`$ から構成した包括関手 $`\gamma`$ がデカルト関手なのは定義から従います。
包括圏の $`\pi : \cat{E}\to \cat{C}`$ は圏のファイブレーションであることを要求しますが、$`\mrm{Cod}: \mrm{Arr}(\cat{C}) \to \cat{C}`$ はファイブレーションである必要はありません。ファイブレーションとは限らない単なる圏のバンドルのあいだでもデカルト関手を考えることはできます（「集合のバンドルと圏のバンドル // デカルト関手とファイバー付き圏」参照）。
エム関手、モデル関手
過去記事「ダラッっと依存型理論・インスティチューション」において、モデル関手は圏 $`\mbf{ComphCAT}`$ の射になるだろう、と書きました。あれはどうも違うようです。モデル関手の条件はけっこうゆるくても大丈夫なようです。
包括圏 $`\msc{K}`$ に対して、ターゲット圏 $`\cat{T}`$ に値をとるエム関手を定義します。「エム関手」はこの文脈におけるテクニカルタームです。インスティチューションのモデル関手のわずかな一般化です。
$`\cat{C}`$ は包括圏 $`\msc{K}`$ のベース圏だとして、関手
$`\quad \msc{M} : \cat{C} \to \cat{T}\In \mbf{CAT}`$
がエム関手〈em functor〉であるとは、以下の関手がデカルト関手であることです。アスタリスク '$`*`$' は関手の結合の図式順演算子記号です。
$`\quad \gamma * \mrm{Arr}(\msc{M}) : \cat{E} \to \mrm{Arr}(\cat{T}) \In \mbf{CAT}`$
$`\mrm{Arr}(\msc{M})`$ はアロー圏のあいだの関手で、関手 $`\msc{M}`$ をアロー圏に持ち上げたものです。
$`\quad \mrm{Arr}(\msc{M}) : \mrm{Arr}(\cat{C}) \to \mrm{Arr}(\cat{T}) \In \mbf{CAT}`$
圏のファイブレーション $`\pi: \cat{E} \to \cat{C}`$ が離散ファイブレーションの場合は次のように言い換えられます。
- $`\cat{E}`$ の任意の射 $`\varphi`$ に対して、 $`\mrm{Arr}(\msc{M})(\gamma(\varphi))`$ は $`\cat{T}`$ のプルバック四角形である。
「任意の射」は離散ファイブレーション特有の話で、一般的には「デカルト射」です。
ν-インスティチューションは包括圏とみなせるので、ν-インスティチューションに対して定義されたエム関手は意味を持ちます。ν-インスティチューション上のエム関手を、習慣に従ってモデル関手〈model functor〉とも呼びます。
ν-インスティチューションの健全性
以上でν-インスティチューションの定義はだいたい説明しました。大事なことは、依存型理論の構文圏〈{syntax | syntactic} category〉である包括圏と、追加のエム関手の性質から、モデル理論的な健全性〈soundness〉が出てくることです。これが本題だったんですが、なんかもう息切れしてきた。
「ν-インスティチューションは健全だ」と言うためには、健全という概念が定義できないとハナシになりません。健全性の記述には、証明可能性〈provability〉と妥当性〈validity〉が必要です。ν-インスティチューションの定義から、証明可能性と妥当性が定義できるのか？ これが出来るんですよ。しかも、依存型理論がベースなので依存性がちゃんと入った形で定義できます。
証明可能性（記号は '$`\vdash`$'）と妥当性（記号は '$`\models`$'）は、ν-インスティチューション $`\msc{K}`$ の内部で定義されて、健全性は、ν-インスティチューション $`\msc{K}`$ を外から見たときのメタ命題です。健全性定理のステートメントは、幾つかのバリアントがあります。以下で、$`\Gamma`$ はコンテキスト（圏 $`\cat{C}`$ の対象）、$`A, B, A_1`$ などは拡張ステップ（エス関手の値である集合の要素）です。記号 '$`\Ent`$' は意味論的伴意〈semantic entailment | 意味論的帰結 | semantic consequence〉、記号 '$`\Imp`$' はメタ命題としての含意〈implication〉です。
- $`\vdash_\Gamma A \;\Imp\; \models_\Gamma A`$
- $`A \vdash_\Gamma B \;\Imp\; A \,\Ent_\Gamma B`$
- $`A_1, \cdots, A_n \vdash_\Gamma B \;\Imp\; A_1, \cdots, A_n \,\Ent_\Gamma B`$
これらのステートメントに出現する「証明可能性」「妥当性」「意味論的伴意」などが、包括圏（としてのν-インスティチューション）とエム関手（モデル関手）の定義だけから組み立てることが可能なのはちょっと驚きです。しかも、ステートメントはメタレベルで証明可能で、任意のν-インスティチューションにおいて実際に成立しています。
で、肝心の「どうやって定義するの？」「どうやって証明するの？」ですが、‥‥ 疲れたのでまたいずれ。
