プロ関手の圏

圏の圏Catの一般化として、プロ関手の圏Profが大事なようだ。

この圏の射＝プロ関手の結合にエンドと余エンドを使うが、エンドと余エンドの双対性を表すには、Σ、Πという記号を使うといいと思う。特に、反転補題（reversing lemma）は自然な形になる。作用積分をeの型に乗せたやつを積積分に展開するのと似ている。

論理の∀、∃、⊃ でも成立しそうだが、よくわからない。