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