------------------------------------------------------------------------ -- The Agda standard library -- -- Sums (disjoint unions) ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Sum.Base where open import Function using (_∘_; _-[_]-_ ; id) open import Relation.Nullary using (Dec; yes; no; ¬_) open import Level using (Level; _⊔_) private variable a b c d : Level A : Set a B : Set b C : Set c D : Set d ------------------------------------------------------------------------ -- Definition infixr 1 _⊎_ data _⊎_ (A : Set a) (B : Set b) : Set (a ⊔ b) where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B ------------------------------------------------------------------------ -- Functions [_,_] : ∀ {C : A ⊎ B → Set c} → ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) → ((x : A ⊎ B) → C x) [ f , g ] (inj₁ x) = f x [ f , g ] (inj₂ y) = g y [_,_]′ : (A → C) → (B → C) → (A ⊎ B → C) [_,_]′ = [_,_] swap : A ⊎ B → B ⊎ A swap (inj₁ x) = inj₂ x swap (inj₂ x) = inj₁ x map : (A → C) → (B → D) → (A ⊎ B → C ⊎ D) map f g = [ inj₁ ∘ f , inj₂ ∘ g ] map₁ : (A → C) → (A ⊎ B → C ⊎ B) map₁ f = map f id map₂ : (B → D) → (A ⊎ B → A ⊎ D) map₂ = map id infixr 1 _-⊎-_ _-⊎-_ : (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d)) f -⊎- g = f -[ _⊎_ ]- g -- Conversion back and forth with Dec fromDec : Dec A → A ⊎ ¬ A fromDec (yes p) = inj₁ p fromDec (no ¬p) = inj₂ ¬p toDec : A ⊎ ¬ A → Dec A toDec (inj₁ p) = yes p toDec (inj₂ ¬p) = no ¬p