{-# OPTIONS --safe #-}

module Data.Bool.Properties where

open import Level
open import Data.Bool
open import Path

if-idem : ∀ (x : A) p → bool x x p ≡ x
if-idem x false = refl
if-idem x true  = refl

open import Data.Unit
open import Data.Empty

true≢false : true ≢ false
true≢false t≡f = subst (bool ⊥ ⊤) t≡f tt

false≢true : false ≢ true
false≢true f≡t = subst (bool ⊤ ⊥) f≡t tt

open import Discrete

module DiscreteBool where
  _≡ᴮ_ : Bool → Bool → Bool
  true  ≡ᴮ y = y
  false ≡ᴮ y = neg y

  complete : ∀ x → T (x ≡ᴮ x)
  complete false = tt
  complete true  = tt

  sound : ∀ x y → T (x ≡ᴮ y) → x ≡ y
  sound false false xy = refl
  sound true true xy = refl

instance
  discreteBool : IsDiscrete Bool
  discreteBool = record { _≟_ = from-bool-eq (record {DiscreteBool}) }

open import HLevels
open import Discrete.IsSet

isSetBool : isSet Bool
isSetBool = Discrete→isSet _≟_

&&-comm : ∀ x y → x && y ≡ y && x
&&-comm false false = refl
&&-comm false true = refl
&&-comm true false = refl
&&-comm true true = refl

&&-idem : ∀ x → x && x ≡ x
&&-idem false = refl
&&-idem true = refl

&&-assoc : ∀ x y z → (x && y) && z ≡ x && (y && z)
&&-assoc false y z = refl
&&-assoc true y z = refl