インスティチューションの仕様圏
インスティチューションのSen(Σ)上にムーア閉包作用素が存在している状況を考える。参考：
A⊆Sen(Σ)を（Σの）仕様、Aが閉包で変わらない（閉じている）ときは（Σの）セオリーと呼ぶことにする。仕様とセオリーは、ほとんど同じものである。
Clを閉包作用素として、仕様AとBのあいだの順序を Cl(A)⊆Cl(B)で定義すると、⊆を射として圏となる。これをSpec(Σ)とする。SpecはSign上のCat値の反変関手になるので、indexed categoryを定義する。このindexed categoryの平坦化圏をSpec(I)（Iはインスティチューション）とする。Σ|→(Σ, Φ)（Φは空仕様）として、ΣをSpec(I)に埋め込むことができる。あるいは、(Σ, A)|→Σを射影とするファイブレーションを定義できる。
ModやSystemを考える際に、SignよりはSpec=Spec(I)の上で考えたほうが自然な気がする。つまりMod((Σ, A))、Prog((Σ, A), (Γ, B))、System((Σ, A), (Γ, B))のようなものを考えることになる。
