コゥゼン圏の定義に加法的ベキ等性を入れると、ホムセットが順序集合になり、局所順序圏になる。となると、コゥゼン圏は2-圏になる。垂直クラスHを導入すると、二重圏にすることもできる。もちろん、最初からモノイド積（双デカルト積）は入っている。とまー…

Esfandiar Haghverdiのプレゼンより：ジラールのGoIは次のようなアナロジーに基づくようだ。 証明的 ジラール曰く 手続き的 関数的 証明 アルゴリズム(algorithm) プログラム 式 cut消去 計算(computation) 実行 評価／簡約 cutなし証明 データ(datum) 結果 …