module Sum where
open import Equality
open import Function
open import Level
infixr 1 _⊎_
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 6 [_∣_]
[_∣_] :
{ℓ ℓ' ℓ'' : 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