{-# OPTIONS --without-K  #-}

module sets.bool where

open import sets.empty     using (⊥)
open import sets.unit      using (⊤)
open import decidable using (Dec; yes; no)
open import equality.core        using (_≡_; refl)
open import level     using (Level)

infixr  _∧_
infixr  _∨_ _xor_
infix   if_then_else_

data Bool : Set where
  true false : Bool

not : Bool → Bool
not true  = false
not false = true

T : Bool → Set
T true  = ⊤
T false = ⊥

if_then_else_ : {a : Level} {A : Set a} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b

_≟_ : (a b : Bool) → Dec (a ≡ b)
true  ≟ true  = yes refl
false ≟ false = yes refl
true  ≟ false = no λ ()
false ≟ true  = no λ ()