インスティチューションにプログラム（のソースコード）とプログラム証明を入れる準備。Pインスティチューションとは、(Sign, Mod, Sen, Prog, PMod, |=)であり、ProgとPModを除くとインスティチューション、Sign⊆Progであり、iが包含として、i;PMod = Mod。…

対称モノイド圏上のモナドFで、Fによるcirc-Kleisli構成のためにF(A)+F(B)→F(A+B)が必要だと書いたが、実際には、モナド単位B→F(B)と組み合わせて、F(A)+B→F(A)+F(B)→F(A+B)として使う。つまり、ほんとに必要なのはF(A)+B→F(A+B)だった。F(A)+B→F(A+B)は、テ…