セオリーと証明の圏
セオリーT⊆Sen(Σ)を対象として、“Tを前提としてS（S⊆Sen(Γ)）を帰結するような証明（図、ネット）”を射とする圏を考える。これはπインスティチューション、ないしはπインスティチューションからModを除いた構造の上で定義できる。この圏をProofとする。α∈Proof(S, T)とは、αが、SからTを導く証明のこと。
まず、Proofが直和で対称モノイド圏になることが欲しい。さらに、有限余完備であれば文句がない。内部セオリー（隠蔽セオリー、作業用セオリー）の概念を導入すれば、（あるいはCirc構成により）Proofをトレース付きモノイド圏にできるだろう。
もし、有限余完備性とトレース付きモノイド圏の両方が成立するなら、Proofからコンパクト閉圏を作る選択肢が2つある。
- Int(GoI)構成
- Cospan構成
この2つの構成を実行して結果を比較できる。
指標Σ、Γに対して適当なプログラミング言語モナドを使ってProg(Γ, Σ)を作れる。Proof(S, T)→Prog(Γ, Σ)という反変（変性はどうでもいいが）関手が定義できるだろう。すると、プログラムの正しさは：
- そのプログラムに対する証明が存在する：構文論的正しさ
- そのプログラムのモデルが存在する：意味論的正しさ
の二通りが定義できて、古典的な概念を再現できそうだ。ここでモデルとは、Mod(Σ)→Mod(Γ)という関手Fだが、FによるMod(S)の像がMod(T)に入るものが正しい（関手意味論、loose semantics）。健全性には、リンデンバウム構成の圏論版が使えるだろう。
