module BoolProofs where open import Bool open import PropositionalLogic open import Identity -- proving equality of two boolean expressions using the equality type notnotI : (x : Bool) → x ≡ not (not x) 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" T : Bool -> Set T true = ⊤ T false = ⊥ -- proving the same equality as above using T notnotT : (x : Bool) → T (x <==> not (not x)) notnotT true = <> notnotT false = <>