ビンゴ！ 「インスティチューションの“指標の圏”の具体化として、型理論的圏の反対圏をとればいいだろう」と見当をつけていたのですが、アタリだったようです。型理論的圏は、拡張包括構造を持ちます。拡張包括構造を持つ圏上の、プルバック四角形（コスパン…