ハイパーインスティチューションに関連すること

1. 当然にインスティチューション
2. 当然に述語論理＝ハイパードクトリン
3. 限量子随伴性 ＝ ΣΔΠ随伴性
4. 否定があるなら、否定双対性。スター自律圏かな？ 継続との関連は？
5. 契約は仕様と関連するから、メイヤー先生のDbCとは関連する。
6. 仕様モジュール、セオリー・モジュールを扱うので、モジュール計算＝大局的プログラミングと関係する。
7. 仕様記述は仕様モジュールの書き方だろう。
8. モデル圏が余代数の圏ならば、模倣、双模倣と関係すると思う。
9. モデル圏のスペクトラムが作れるのでは？
10. リンデンバウム構成と判断〈judgement〉
11. 高次圏論とストリング論理
12. ホーア式とホーア論理
13. コンピュータッド＝生成系＝プレゼンテーション

あらためてハイパードクトリンを定義すると：まずドクトリンDがある。値の"圏の圏”としてDを取るインデックス付き圏の全体を IndCat<D>とする。ベース圏がCであるインデックス付き圏の全体は、IndCat<D>[C]。

• IndCat<D>に含まれるインデックス付き圏をD-プレ・ハイパードクトリンと呼ぶ。
• プレ・ハイパードクトリンがΣΔΠ随伴性を持つとき、D-ハイパードクトリンと呼ぶ。
• ドクトリンDが論理的であると仮定するが、論理的の定義はないので、具体的にCCCとかDCCCなどのドクトリンを取って議論する。
• インデックス付き圏よりファイバー圏で議論するほうが良いのかも知れない。