------------------------------------------------------------------------ -- 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 (_⊔_) ------------------------------------------------------------------------ -- Definition infixr 1 _⊎_ data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B {-# FOREIGN GHC type AgdaEither a b c d = Either c d #-} {-# COMPILE GHC _⊎_ = data AgdaEither (Left | Right) #-} ------------------------------------------------------------------------ -- Functions [_,_] : ∀ {a b c} {A : Set a} {B : Set b} {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 b c} {A : Set a} {B : Set b} {C : Set c} → (A → C) → (B → C) → (A ⊎ B → C) [_,_]′ = [_,_] swap : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → B ⊎ A swap (inj₁ x) = inj₂ x swap (inj₂ x) = inj₁ x map : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → (A → C) → (B → D) → (A ⊎ B → C ⊎ D) map f g = [ inj₁ ∘ f , inj₂ ∘ g ] map₁ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}→ (A → C) → (A ⊎ B → C ⊎ B) map₁ f = map f id map₂ : ∀ {a b d} {A : Set a} {B : Set b} {D : Set d} → (B → D) → (A ⊎ B → A ⊎ D) map₂ = map id infixr 1 _-⊎-_ _-⊎-_ : ∀ {a b c d} {A : Set a} {B : Set b} → (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d)) f -⊎- g = f -[ _⊎_ ]- g module _ {p} {P : Set p} where -- Conversion back and forth with Dec fromDec : Dec P → P ⊎ ¬ P fromDec (yes p) = inj₁ p fromDec (no ¬p) = inj₂ ¬p toDec : P ⊎ ¬ P → Dec P toDec (inj₁ p) = yes p toDec (inj₂ ¬p) = no ¬p