ハイパーインスティチューションの大事なこと

重要なのはグロタンディーク／エルブラン圏である。

MLの概念	グロタンディーク／エルブラン圏	別な言い方
シグニチャー	仕様	セオリー
ストラクチャ	絶対セオリー	インスタンス
ファンクタ	相対セオリー	トランスフォーマー
シグニチャに属するストラクチャ	仕様を満たす絶対セオリー	セオリーのインスタンス

ストラクチャ／絶対セオリー／インスタンスは、インスティチューションのモデルになる。モデル射は、ひとつのシグニチャ／仕様の自己トランスフォーマーの特殊なもの。一般のトランスフォーマーにより、モデル圏のリダクト関手が定義される。リダクト関手は、指標射＝トランスフォーマーで誘導される。

仕様の指標部で、定数名、関数名、述語名（基本命題名）が定めるから、対応する論理言語の論理式としてSen[Σ]が決まる。仕様の命題部でSen(Σ)は既に使っている。Mod[Σ]の作り方から言って、X∈|Mode[Σ]| は仕様の命題部の命題をすべて充足している。しかし、Sen[Σ]のその他の命題は、充足する保証はない。

ハイパーインスティチューション（あるいはグロタンディーク／エルブラン・インスティチューション）のモデル圏は、エルブラン・モデルとして定義される（だからエルブランを冠している）。

• ドクトリン → ベック（by Jon Beck）
• ハイパードクトリン → ローヴェル（Bill Lawvere）
• 平坦化／ファイバー化 → グロタンディーク（Alexander Grothendieck）
• 構文的項モデル → エルブラン（Jacques Herbrand）

グロタンディーク／エルブラン圏は、有限余完備圏である。が、直和がモノイド積としては与えることができない。直和や融合和（プッシュアウト、余ファイバー和）はup-to-isoで作ることができる。up-to-isoのisoを与えているのはリネーミング同型射である。

• up-to-iso ＝ up-to-rename

これは非常に重要な知見である。up-to-renameはラムダ計算のα変換と同じだし、名前の影響は無視して良いことを示している。大局的プログラミングにおけるモジュール演算は、すべてup-to-renameで構成されるもので、確定的演算ではない！