ネタ

メモ編ネタがあるときは本編ネタがなくなる。まー、そういうもんだな。

メモ編ネタ：

1. Programming in the Hugeをやりたい。
2. 仕様証明とプログラム証明は別物だ。ちゃんと区別。仕様証明はπインスティチューションの概念、プログラム証明はπPインスティチューションの概念。
3. 3変項関手F(A, B, X)=(B×X)^Aがあると、F(A, B, -)余代数の圏ができるが、Fからモナドと適当なKleisli圏が作れて、homsetは余代数の圏となる、したがって2-圏構造を持つ。終余代数を選び出すと、余代数でenrichされた圏ができる、たぶん。
4. テンソル強度、関手強度、モナド／コモナド分配法則、ペアリング、enrichment、indexed categoryって、どんな関係？