まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }`$
| コンテナ | インスティチューション |
|---|---|
| シェイプ（単なる原子記号） | 指標（コンピュータッド構造） |
| シェイプの集合 | 指標圏 |
| シェイプのポジション集合 | 指標のセオリー（生成された圏） |
| 値の集合 | ターゲット圏 |
| マップデータ（関数） | モデル（関手） |
| 単純単項式（集合） | モデルの圏 |
| コンテナ関手 | モデル関手（2-関手） |
コンテナ関手＝多項式関手：
$`\quad X \mapsto \sum_{s\in S}X^{P(s)}
: {\bf SET} \to {\bf SET}
`$
モデル関手：
$`\quad \cat{T} \mapsto \coprod_{\Sigma \in \cat{S}} [ \mrm{Theo}^L (\Sigma), \cat{T}]
: {\bf CAT} \to {\bf CAT}
`$
Mizar用語を拝借して、モジュールを「アーティクル」ということにする。$`A`$ が指標 $`\Sigma`$ 上のアーティクルだとは：
$`\quad A \subseteq \underline{\mrm{Theo}^L (\Sigma)}, \; \Sigma\subseteq A`$
のこと。ここで、下線は忘却関手を表し、圏の台有向グラフのこと。
アーティクルの集まりをライブラリ（またはリテラチャー）と呼ぶ。ライブラリが知識コンテキストを作り。他のアーティクル（グリモワ）やステージの土台となる。
リーズニングゲームは、ライブラリとスキルボックス＝コマンドセットにより構成される。ライブラリとコマンドセットが背景環境を定義する。クエストのアウトカム〈産物〉として新しい定理を手に入れる。アウトカムは、ライブラリに反映してよい。あるいは新しいアーティクルにしてもよい。クエストにより、ライブラリは進化〈evolv〉する。
複雑な指標の構造はバンチで記述する。適当なベース圏の上のバンチの構文的圏を作り、バンチ射＝広義シーケントを射とする多圏ができる。複圏＝オペラッドを中間に入れると分かりやすい。バンチの複圏と、バンチの多圏がある。バンチ複射をバンチ構成してバンチ多射を作れる。
