「インスティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。 ホーア論理の圏論的な定式化 真偽構造が付いた圏 -- ホーア論理のために 「インデックス付き圏のフビ…