{-# 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
infixr 1 _⊎_
data _⊎_ (A : Set a) (B : Set b) : Set (a ⊔ b) where
inj₁ : (x : A) → A ⊎ B
inj₂ : (y : B) → A ⊎ 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 → 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 1 _-⊎-_
_-⊎-_ : (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d))
f -⊎- g = f -⟪ _⊎_ ⟫- g
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