n-タイプの基本構図

まず、同義語のまとめ。

• 指標⊆仕様＝セオリー＝プレゼンテーション＝コンピュータッド＝ポリグラフ＝グラフ＝箙
• モデル＝構造＝代数＝加群＝表現

基本構図は：

• A ∈₀ n-Alg^D(τ, A)

これの文脈は、

• τ ∈₀ n-Thy
• D ∈₀ (n+1)-Thy
• A ∈₀ (n+1)-Alg^D'(τ', A')

文脈内に同じ形が出てくるのはマイクロコスモ原理による。τ', D', A' がまた1次元上の基本構図を作る。それが無限に続く。

用語法、あるいは呼び名。

• n-Alg^D(τ, A) を、代数的n-型〈n-タイプ〉、またはn-クラスと呼ぶ。
• Aを、このn-型〈n-クラス〉のn-インスタンスと呼ぶ。nが明らかなら、単にインスタンスでもよい。
• Dを、このn-型のn-ドクトリンと呼ぶ。nが明らかなら、単にドクトリンでもよい。
• τを、このn-型のn-セオリーと呼ぶ。nが明らかなら、単にセオリーでもよい。
• Aを、このn-型のn-アンビエントと呼ぶ。nが明らかなら、単にアンビエントでもよい。

基本構図を2階層重ねると：

• [n+1] A ∈₀ (n+1)-Alg^D'(τ', A')
• [n] A ∈₀ n-Alg^D(τ, A)

この文脈で、次のタイプ-インスタンス原理〈type-instance principle〉が言える。

• n-Alg^D(τ, A) ∈₀ (n+1)-Alg^D'(D, A') （適当なメタドクトリンD'とメタアンビエントA'のもとで）

これは、(n+1)圏であるn-Catにおいて指数構成が可能（デカルト閉）であることの帰結である。

タイプ-インスタンス原理は、"a type is an instance"を意味する。次元を明示すれば、"an n-type is an (n+1)-instance"。nは何でもいいので、

• 0-type is 1-instance
• 1-type is 2-instance
• 2-type is 3-instance
• … …

一度は滅んだラッセル流の階層的タイプ理論の復活だと言えなくもない。ラッセルが型階層をうまく作れなかったのは、高次圏論がなかったからだろう、後知恵で言えば。