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

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Sum.Base where

open import Data.Bool.Base using (true; false)
open import Function.Base using (_∘_; _∘′_; _-⟪_⟫-_ ; id)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
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  _⊎_

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 ]′

reduce : A ⊎ A → A
reduce = [ id , 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

assocʳ : (A ⊎ B) ⊎ C → A ⊎ B ⊎ C
assocʳ = [ map₂ inj₁ , inj₂ ∘′ inj₂ ]′

assocˡ : A ⊎ B ⊎ C → (A ⊎ B) ⊎ C
assocˡ = [ inj₁ ∘′ inj₁ , map₁ inj₂ ]′

infixr  _-⊎-_
_-⊎-_ : (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 ( true because  [p]) = inj₁ (invert  [p])
fromDec (false because [¬p]) = inj₂ (invert [¬p])

toDec : A ⊎ ¬ A → Dec A
toDec (inj₁ p)  = yes p
toDec (inj₂ ¬p) = no ¬p