module Sum where

open import Equality
open import Function
open import Level

----------------------------------------------------------------------
-- Disjoint union
----------------------------------------------------------------------
infixr  _⊎_
data _⊎_ {ℓ ℓ' : Level}(L : Set ℓ)(R : Set ℓ') : Set (ℓ ⊔ ℓ') where
  inl : (x : L) → L ⊎ R
  inr : (y : R) → L ⊎ R

inlInj :
  {ℓ ℓ' : Level}
  {L : Set ℓ}
  {R : Set ℓ'}
  {x x' : L}
  → -----------------------------
  inl {R = R} x ≡ inl x' → x ≡ x'
inlInj refl = refl

inrInj :
  {ℓ ℓ' : Level}
  {L : Set ℓ}
  {R : Set ℓ'}
  {y y' : R}
  → ------------------------------
  inr {L = L} y ≡  inr y' → y ≡ y'
inrInj refl = refl

infix  [_∣_]
[_∣_] :
  {ℓ ℓ' ℓ'' : Level}
  {L : Set ℓ}
  {R : Set ℓ'}
  {A : Set ℓ''}
  (f : L → A)
  (g : R → A)
  → ---------------
  L ⊎ R → A
[ f ∣ g ] (inl x) = f x
[ f ∣ g ] (inr y) = g y