{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Sum.Base where

open import Cubical.Relation.Nullary

open import Cubical.Core.Everything

private
  variable
     ℓ' : Level
    A B C D : Type 

data _⊎_ (A : Type )(B : Type ℓ') : Type (ℓ-max  ℓ') where
  inl : A  A  B
  inr : B  A  B

rec : {C : Type }  (A  C)  (B  C)  A  B  C
rec f _ (inl x) = f x
rec _ g (inr y) = g y

elim : {C : A  B  Type }   ((a : A)  C (inl a))  ((b : B)  C (inr b))
        (x : A  B)  C x
elim f _ (inl x) = f x
elim _ g (inr y) = g y

map : (A  C)  (B  D)  A  B  C  D
map f _ (inl x) = inl (f x)
map _ g (inr y) = inr (g y)

_⊎?_ : {P Q : Type }  Dec P  Dec Q  Dec (P  Q)
P? ⊎? Q? with P? | Q?
... | yes p | _ = yes (inl p)
... | no _  | yes q = yes (inr q)
... | no ¬p | no ¬q  = no λ
  { (inl p)  ¬p p
  ; (inr q)  ¬q q
  }