module Prelude.Sum where
open import Prelude.Level
----------------------------------------------------------------------
-- Disjoint union
----------------------------------------------------------------------
infixr 6 _⊎_
data _⊎_ {l m : Level}(A : Set l)(B : Set m) : Set (l ⊔ m) where
ι₁ : (x : A) → A ⊎ B
ι₂ : (y : B) → A ⊎ B
----------------------------------------------------------------------
-- Disjunction
----------------------------------------------------------------------
infixr 2 _∨_
_∨_ : {l m : Level}(A : Set l)(B : Set m) → Set (l ⊔ m)
_∨_ = _⊎_