module Booleans where
open import Preliminaries
abstract
left right : {A B : Set} → A + B → Set
left (inl _) = ⊤
left (inr _) = ⊥
right t = left (+-symm .fun t)
left-right-disj : {A B C : Set} {t : A + B} → left t → right t → C
left-right-disj {t = inl _} _ ()
left-prop : {A B : Set} {t : A + B} → isProp (left t)
left-prop {t = inl _} = ⊤-prop
right-prop : {A B : Set} {t : A + B} → isProp (right t)
right-prop = left-prop
left-or-right : {A B : Set} (t : A + B) → isContr (left t + right t)
left-or-right (inl _) .fst = inl tt
left-or-right (inr _) .fst = inr tt
left-or-right _ .snd = +-prop left-prop left-prop left-right-disj _
left-intro : {A B : Set} {a : A} → left {B = B} (inl a)
left-intro = tt
right-intro : {A B : Set} {b : B} → right {A = A} (inr b)
right-intro = tt