module Bool where open import Logic data Bool : Set where true false : Bool if_then_else_ : {A : Set} → Bool → A → A → A if true then x else y = x if false then x else y = y IsTrue : Bool → Set IsTrue true = ⊤ IsTrue false = ⊥ not : Bool → Bool not true = false not false = true _&&_ : Bool → Bool → Bool true && x = x false && _ = false _||_ : Bool → Bool → Bool true || _ = true false || x = x