ハイパーインスティチューションの構造と用語法

指標（"インデキシング・ベース圏”の対象）と命題（{インデキシング垂直圏 | ファイブレーションのファイバーである圏}の対象）のペアを仕様と呼ぶ。仕様はグロタンディーク／エルブラン圏＝ハイパーベース圏の対象であると同時に、ハイパーインスティチューションのモデル圏のコンピュータッド＝生成系＝プレゼンテーションになっている。

指標は、命題部分が自明な仕様なので、指標を仕様に埋め込める。仕様は、構造〈インスタンス | 絶対セオリー | 基礎セオリー〉に対する公理的規定〈axiomatic {regulation | standard | norm}〉（定義とは言わない！）を与える。仕様の命題部分から導出閉包（導出される命題の反射的推移的閉包）を作れる。導出閉包には証明（定理〈論理射〉の定義ボディ〈定義項〉）が必要、証明〈定理項 | 定理の定義ボディ〉を作るには、証明構成手続き（基本手続きは推論規則）が必要。よって、背後に推論規則セットがある。

推論規則は、論理圏〈命題と定理の圏〉の2-射となる。論理圏は必然的に2-圏である。0-射＝命題／述語、1-射＝定理／公理、2-射＝推論手続き／推論規則 である。

仕様には、推論規則を入れもよくて、そうなると：

1. 型のプロファイリング： 指標圏〈インスタンス・ベース圏〉の対象
2. 値〈データ〉のプロファイリング： 指標圏の基礎射
3. 関数のプロファイリング： 指標圏の射
4. 命題のバインディング： 論理圏の対象の命名
5. 推論手続きのプロファイリング： 論理圏の2-射

利用者観点では：

1. 使ってよい指標圏の対象＝S0-セル
2. 使ってよい指標圏の基礎射＝S1-セル（特殊）
3. 使ってよい指標圏の射＝S1-セル
4. 使ってよい論理圏の基礎射＝L1-セル（特殊）
5. 使ってよい論理圏の2-射＝L2-セル

あれれ、「L0-セル＝使ってよい論理圏の対象」がない。考え直さないと。←課題

グロタンディーク／エルブラン圏を整理すると：

• 対象は、セオリー仕様である。利用者視点では「使ってよい射＝セル」の集合。構成者視点では、「作るべき射」の集合。
• 基礎射は、セオリーインスタンスである。
• 一般の射は、セオリートランスフォーマーである。

となると：

• 対象を仕様と呼ぶ。
• 基礎射をインスタンス（事例）と呼ぶ。
• 一般の射をトランスフォーマー（変換子）と呼ぶ。

英語	漢字	カタカナ
spec, specification	仕様	スペック、スペシフィケーション
instance	事例	インスタンス
transformer	変換子	トランスフォーマー、トランスフォーマ

射の呼び名：

	指標圏	論理圏	GH圏＝セオリー圏
0-セル	基本型	述語、基本命題	基本仕様
0-基礎射	ユニット型	真	ユニット仕様
0-射	型	命題	仕様
1-セル	基本関数	公理	基本仕様
1-基礎射	値、定数	公理	インスタンス
1-射	関数	定理	トランスフォーマー
2-セル	スキーマ	推論規則	-
2-基礎射	-	公理規則	-
2-射	-	推論手続き	-

アンビエント圏、指標圏、論理圏、セオリー圏＝グロタンディーク／エルブラン圏はなんらかのドクトリンのなかに居る。例えば：

• アンビエント圏 : 基礎付き両デカルト・モノイド閉圏
• 論理圏 : 基礎付き両付点デカルト・モノイド閉圏＋2-圏構造
• セオリー圏 ： 基礎付き有限余完備圏

所属するドクトリンによって、「何ができるか」かが決まる。

課題：系統的に仕様すべき形容詞の用法を決める。

• 基本、原始、組み込み、単純、複合〈compound | composite | composed | mixed | complex〉
• 絶対、相対
• 基礎、応用