ハイパードクトリンとセオリー圏

Sを指標圏、Lを論理ドクトリンとするハイパードクトリンH:S→Lがあるとする。Σ∈|S| に対してH[Σ]は指標Σ上の論理圏であり、その論理圏は論理ドクトリンLに所属する。

ハイパードクトリンHをインデックス付き圏とみなして、そのグロタンディーク平坦化をTheo(H)とする。Th(H)を、Hのセオリー圏と呼ぶ。グロタンディーク平坦化は任意のインデックス付き圏に対して行えるので、セオリー圏は確実に構成できる。

セオリー圏の対象は、指標Σと命題Aのペア(Σ, A)となる。これを仕様〈specification〉と呼ぶ。セオリー圏の射は、指標射と証明のペアであるが、これをセオリー〈theory〉と呼ぶ。セオリー T:A→B in Theo(H) に対して、dom(T)をTの要求〈requiment〉、cod(T)をTの保証〈assurance〉と呼ぶ。

指標圏に特定された始対象0があり、各論理権にも特定された終対象1_Σがあるとする。(0, 1₀)で定義される仕様を自明仕様〈trivial specification〉と呼びΘで表す。

T:Θ→S の形のセオリーを絶対セオリー〈absolute theory〉または基礎セオリー〈ground theory〉と呼ぶ。絶対でないセオリーは相対セオリー〈relative theory〉、または応用セオリー〈applied theory〉と呼ぶ。セオリーが基礎セオリーであることを"グランドしている”〈grounded〉とも言う。相対セオリー〈応用セオリー〉はグランドしてない。

ハイパードクトリン（さらにはハイパーインスティチューション）から作られるセオリーの圏の構造を把握すれば、STEM記述フレームワークの基礎が固まるだろう。

用語の比較：

論理	オブジェクト指向	関数型
指標	インターフェイス	型クラス
仕様	表明付きインターフェイス	表明付き型クラス
絶対セオリー	クラス	インスタンス
相対セオリー	なし	MLのファンクタ？

パッケージ／モジュールと、仕様／セオリーは独立な概念であるが、管理単位と論理単位を一致させるなら：

• 仕様（spec）モジュールで仕様を記述する
• セオリー（theo）モジュールでセオリーを記述する
• パッケージでセオリー圏の部分圏を記述するする
• パッケージマネージャで、部分圏を変更する。
• ストレージに存在するライブラリも部分圏を記述する。

課題：ハイパードクトリン、ハイパーインスティチューション、セオリー圏を探求せよ。