```------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums (disjoint unions)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Sum.Base where

open import Function.Base 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)
[_,_]′ = [_,_]

fromInj₁ : (B → A) → A ⊎ B → A
fromInj₁ = [ id ,_]′

fromInj₂ : (A → B) → A ⊎ B → B
fromInj₂ = [_, id ]′

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
```