module Data.Bool.Base where

true≠false : ¬ true ≡ false
true≠false p = subst P p tt where
  P : Bool → Type
  P false = ⊥
  P true = ⊤

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

and or : Bool → Bool → Bool
and false y = false
and true y = y

or false y = y
or true y = true

instance
  Discrete-Bool : Discrete Bool
  Discrete-Bool {false} {false} = yes refl
  Discrete-Bool {false} {true}  = no false≠true
  Discrete-Bool {true}  {false} = no true≠false
  Discrete-Bool {true}  {true}  = yes refl

x≠true→x≡false : (x : Bool) → x ≠ true → x ≡ false
x≠true→x≡false false p = refl
x≠true→x≡false true p = absurd (p refl)

x≠false→x≡true : (x : Bool) → x ≠ false → x ≡ true
x≠false→x≡true false p = absurd (p refl)
x≠false→x≡true true p = refl

is-true : Bool → Type
is-true true  = ⊤
is-true false = ⊥

record So (b : Bool) : Type where
  field
    is-so : is-true b

pattern oh = record { is-so = tt }