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