module Booleans where

open import Preliminaries

abstract
  -- An instance of descent/large elimination for binary coproducts.
  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