二重圏上のインスティチューション

指標圏に境界概念とグルーイングを導入して、コボルディズム的な二重圏だと考える。インスティチューションをこの二重圏の上で定義する。すると、Mod、Sen、Spec、Theo（Sen上に作る順序集合）なども拡張されるだろう。

さらに、証明系ProofやプログラムProgも拡張する。それで、プログラミング行為全般を説明できるんじゃないか？ （まだ足りないかもしれないが。）BHKのコンストラクタ項とかエルブラン空間の概念により、XML（データ代数）の構文論も取り込みたい。