module BoolProofs where

open import Bool
-- open import PropositionalLogic
open import Identity

-- proving equality of two boolean expressions using the equality type

notnotI : (b : Bool) → b ≡ not (not b)
notnotI true = refl
notnotI false = refl

-- notnotI x = if x then refl else refl

-- turning boolean into set so that true maps to an inhabited set and false maps to an empty set,
-- the isTrue-predicate "So"

So : Bool -> Set
So true = {!⊤!}
So false = {!!}

-- proving the same equality as above using T

_<==>_ : Bool → Bool → Bool
true <==> true = true
true <==> false = false
false <==> true = false
false <==> false = true

sonotnot : (b : Bool) → So (b <==> not (not b))
sonotnot true = {!!}
sonotnot false = {!!}