インスティチューションの構成的精密化
インスティチューションでは、指標Φに対してモデル圏Mod[Φ]が決まる。まーこれはいいのだが、指標圏が何であるか、Mod[Φ]をどう作るかは言及しない。公理的フレームワークだから、まー、そんなもんだ。しかし実際に出現するインスティチューションではもっと細かな構成をしなくてはならない。
その構成の方法：
基礎圏（ground category）が必要。多くの場合はSetが基礎圏。たくさんの圏が登場するが、それらはすべて基礎圏の上の具象圏、つまり唯一の忠実な忘却関手を持つ。基礎圏をBとすると、具象圏の圏は、オーバー圏 CAT/Bの部分圏になる。
指標Φごとに、アンビエント圏Amb[Φ]が決まる。正確に言うと、アンビエント圏ではなくてアンビエント・オペラッド。Φからオペラッドを作る。その作り方を示す。
指標は、他の指標に依存する。Mod[Φ]の作り方が階層的帰納的構成になっている。指標Φが参照している指標をΨ1, ..., ΨNのN個だとする。対応するモデル圏を Ci := Mod[Ψi] とする。
C1, ..., CN からオペラッドOpd[C1, ..., CN] を作る。
O := |C1| + ... + |CN| として、これをオペラッドの対象類とする。A1, ..., An, B∈|O| にたいして、オペセット Op([A1, ..., AN], B) を次のように定義する。
オペラッドの結合や単位は、基礎圏に帰着させれば定義できる。
アンビエント・オペラッドが定義できれば、指標からアンビエント・オペラッドへのオペラッド関手としてモデルを定義できる。オペラッド関手のあいだのオペラッド自然変換としてモデルの射が定義できて、モデル圏が定義できる。
モデル圏に忘却関手を定義できる。忘却関手の行き先は指標のソート数（キャリア数）をnとしてBnになる。指標のソート数は非常に基本的な量であある。0-ソートの指標は1個しかなくて、そのモデル圏は単位圏となる。ソート数が1の指標が単ソート指標。
実際はもっと複雑で、基礎圏Bはデカルト閉圏で、出てくる圏はすべてB-豊饒圏となっている。固定したBに対する豊饒デカルト閉圏の理論が必要になる。
さらに、Senを定義するための論理言語だけではなくて、式（関数項）を定義するためのプログラミング言語が必要になる。指標の圏は、プログラミング言語の構文が定義するモナドが作用することになる。このモナドは、式の自由生成と忘却関手による随伴対から作られるモナドになっている。
インスティチューションに、オペラッド、豊饒圏、構文モナドを混ぜて考える必要がある。
