なんでコンパクト閉圏かと言えば、Janus（ヤヌス）コンポネントを考えたら自然に必然的にコンパクト閉圏になるからだ。で、絵の向きがあらためて気になって仕方ない。典型的な例として、モデルとエンジンからなるプラットフォーム（DOMとか）とUIにはさまれ…

以前、Pow(Sen(-))という関手をindexed categoryだとみなして、それを平坦化してSpecを定義した。SystemはSpec上で定義した方が自然だろうから、Γ、Σは指標じゃなくて仕様だとしてSystem(Γ, Σ)は「Γを満たす実装を渡されてΣを満たすような実装」となる。Prog…

とにかくメモ、しゃべるようにメモじゃ。インスティチューションのMod関手を一般化したい。指標Σ、Γと指標射φがあるとき、Mod(φ): Mod(Γ)→Mod(Σ) となるが通常のMod関手だが、Modを2引数Mod(Γ, Σ)にしたいのだが、混乱をさけるため2引数のバージョンはSystem…