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