data Bool : Set0 where true : Bool ; false : Bool data _∨_ (A : Set0) (B : Set0) : Set0 where intro1 : A -> A ∨ B intro2 : B -> A ∨ B data Id {A : Set0} : A -> A -> Set0 where refl : (a : A) -> Id a a -- Boolはなぁ・・・trueか、falseだけな…

http://journal.mycom.co.jp/news/2009/10/30/087/index.htmlと思ったけど、PSPはついてないんですね。まぁPSP買っても良いかなーみたいなソレはどうしよう。12/3って確実に悲しい生活に陥ってるので何をやるにしても年末だよなぁみたいな。