日記風にダラッと書きます。
ヴォエヴォドスキー〈Vladimir Voevodsky〉のC-システム（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）は、名前を変更しただけでカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉と同じものです。カートメルはまた、一般化代数セオリー〈generalized algebraic theory〉を提案しています。コンテキスト圏も一般化代数セオリーも、1978年のカートメルの学位論文内で定義されたものです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in }}
\newcommand{\GAT}{\mathsf{GAT} }
`$
一般化代数セオリーは、ローヴェアの代数セオリーを一般化したものです。「ローヴェア・セオリーとその周辺 」でも書いたように、「セオリー」という呼び名はトラブルのもとです。GAT〈ガット〉をひとつの名詞として扱い、「セオリー」は「T」一文字に閉じ込めて表に出ないようにしましょう。この伝でいうと、オリジナルのローヴェア代数セオリーもLAT〈ラット〉と呼び「セオリー」は出さないのがよいですね。
形式体系としてのGATを、サンセリフ体で $`\GAT`$ と書くことにします。「球体集合達の圏の構文表示 2/2」において、球体集合達の圏を表現するための形式体系を $`{\mathsf{Glob} }`$ と書いたのと同じ記法の約束です。
形式体系 $`\GAT`$ については、次の論文のはじめのほうに書いてあります。
- [Ste19-]
- Title: Algebraic Type Theory and Universe Hierarchies
- Author: Jonathan Sterling
- Submitted: 23 Feb 2019
- Pages: 25p
- URL: https://arxiv.org/abs/1902.08848
上記のスターリング論文内では「セオリー」が使われています。ウムー😟
スターリングのセオリーは、通常の型システム（型理論的形式体系）の言葉で言えばコンテキストのことです。$`\GAT`$ では、コンテキストをニ種類に分ける必要があるのです。ここでは、ベースコンテキスト〈base context〉と局所コンテキスト〈local context〉としましょう。スターリングは、ベースコンテキストを「セオリー」、局所コンテキストを「テレスコープ」と呼んでいます。
「指標の圏はコンテキストの圏の反対圏」で述べたように、コンテキストと指標は同じものです（そう考えてかまわない）。コンテキストの圏（型システムの構文圏）と指標の圏は互いに反対圏の関係にありますが、対象達は同一なので「コンテキスト ＝ 指標」です。
形式体系 $`\GAT`$ の構文代数系（「型理論的形式体系の構文代数系はファイバー付き依存多圏」参照）が、単なる圏ではなくて、ファイブレーション構造を持った圏類似代数系〈category-like algebraic system | CLAS〉なのです。ファイブレーション構造があるということは、ベース空間／ファイバー空間達／トータル空間があるということです（「空間」の使い方は「変換手意味論とブラケット記法 // 「空間」という言葉」参照）。
$`\GAT`$ の構文代数系は、ファイバー付き圏とは若干違う圏類似代数系になるようです（「型理論的形式体系の構文代数系はファイバー付き依存多圏」参照）が、ファイバー付き圏の用語を借用して語ることにします； ベース対象（ベース圏の対象）がベースコンテキストで、ファイバー対象（ファイバー圏（ファイバー付き圏ではない！）の対象）が局所コンテキストです。ファイバー対象はトータル圏の対象でもあるので、ファイバー対象はトータル対象でもあります。
「最近の型理論： 拡張包括構造を持ったインデックス付き圏」において、ファイバー圏と同じ意味の局所圏〈local category〉という言葉を導入しています。その事情は：
局所圏 $`\cat{P}[X]`$ はファイバー圏〈{fibre | fiber} category〉とも言えますが、ファイバー付き圏〈{fibred | fibered} category〉と紛らわしいので「局所圏」としました。
「局所」と対になる「大域」を使って「大域圏」と言いたくなりますが、ベース圏のことかトータル圏のことか判然としないので「大域圏」は使いません。局所圏〈ファイバーである圏〉は次の記法で表します。
「環境付き計算と依存アクテゴリー 1/n」より：
対象 $`S\in |\cat{S}|`$ に対する関手 $`\mrm{Proj}`$ の逆像は、$`S`$ 上のファイバー〈fiber | fibre〉または局所圏〈local category〉と呼び、次のように書きます。
$`\quad \cat{E}_{@S} := \mrm{Proj}^{-1}(S) \; \In {\bf CAT}`$
$`\GAT`$ の構文代数系は、次の形のファイブレーションだとします。
$`\quad \xymatrix{
\cat{G} \ar[d]^{\mrm{Proj}}
\\
\cat{B}
}
`$
ベース対象＝ベースコンテキストは、一般代数学〈universal algebra〉やインスティチューション理論の意味の指標です。ただし、指標の記述に依存型が使えます。つまり、依存指標〈dependent signature〉ということになります。モノイドの指標は依存型なしで書けますが、ホムセットベースの小さい圏の指標は依存型がないとうまく書けません。その意味で、GATのベース指標はLATの指標（単ソート代数的指標）に比べて記述力が向上しています。
ベース対象〈ベースコンテキスト | ベース指標〉 $`\Gamma \in |\cat{B}|`$ をひとつ選ぶと、局所圏（正確には、局所・圏類似代数系） $`\cat{G}_{@\Gamma}`$ が決まります。この局所圏（局所・構文代数系）はC-システムになります。したがって、局所コンテキストはC-システムの対象ということになります。
ここまで説明したことにより、スターリング〈Jonathan Sterling〉の用語は次のように説明できます。
- スターリングのセオリー： $`\GAT`$ の構文代数系のベース対象
- スターリングのテレスコープ： $`\GAT`$ の構文代数系の局所対象
C-システムは型システムの構文代数系でした。なので、$`\GAT`$ の構文代数系は、“たくさんの型システムの構文代数系達を束ねた形の構文代数系”ということになります。入れ子構造／階層構造を持つ構文代数系なのです。入れ子といえばスノーグローブ現象を思い出します。
「複前層の圏とファミリー付き圏」より：
またしてもスノーグローブ現象（「依存アクテゴリーに向けて // スノーグローブ現象／マイクロコスモ原理」「マイクロコスモ原理と逆帰納ステップ」参照）に出会っている気がします。スノーグローブ現象を積極的に利用した応用や手法があるのかも知れません。
十分に記述力が高い形式体系では、（ゲーデル・コード化のような）自己参照コード化により自分自身について語ることができるはずです。GATが持つ入れ子構造は、スノーグローブ現象の定式化を可能にするかも知れません。
