2007-10-05 業務研究、今週のまとめ: Agda 実は Agda の上で impredicative な議論が強力に展開できるということ、そして証明論的にはアホみたいに強いということ。驚きました。