SignからSpecへの持ち上げ

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

Prog(Σ, Γ)もSpec上で定義すれのは簡単だ。あとは、証明と証明変換をSpec上で定義すればいいような気がする。