open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base

module Data.Sum.Base where


# Sum typesπ

Sum types are one of the fundamental ingredients of type theory. They play a dual role to the product type; if products allow us to state that we have elements of two types simultaneously, sum types allow us to state that we have an element of one of two types.

We use the notation A β B to hint at this typeβs set-theoretic analog: the disjoint union.

infixr 3 _β_

data _β_ {a b} (A : Type a) (B : Type b) : Type (a β b) where
inl : A β A β B
inr : B β A β B

private variable
a b c d : Level
A B C D : Type a


## Universal propertiesπ

One of the most important things about sum types is the following property: given two functions A β C and B β C, we can construct a function A β B β C.

[_,_] : (A β C) β (B β C) β (A β B) β C
[ f , g ] (inl x) = f x
[ f , g ] (inr x) = g x

infix 0 ifβΊ_then_else_

ifβΊ_then_else_ : A β B β C β C β C
ifβΊ inl _ then y else n = y
ifβΊ inr _ then y else n = n


Furthermore, this function is βuniversalβ in the following sense: if we have some function h : A β B β C that behaves like f when provided an inl a, and like g when provided inr b, then h must be identical to [ f , g ].

[]-unique : β {f : A β C} {g : B β C} {h} β f β‘ h β inl β g β‘ h β inr β [ f , g ] β‘ h
[]-unique p q = funext Ξ» { (inl x) i β p i x ; (inr x) i β q i x }


We also have the following eta law. In general, eta laws relate the introduction forms with the elimination forms. The most familiar eta law is the one for functions: Ξ» x β (f x) is the same as f. In agda, the eta law for functions requires no proof, it holds by definition. However, the same cannot be said for sum types, so we prove it here.

[]-Ξ· : β (x : A β B) β [ inl , inr ] x β‘ x
[]-Ξ· (inl x) = refl
[]-Ξ· (inr x) = refl


This universal property can be strengthened to characterising the space of dependent functions out of the disjoint union: A dependent function (x : A β B) β P x is the product of functions covering the left and right cases.

β-universal : β {A : Type a} {B : Type b} {C : A β B β Type c}
β ((x : A β B) β C x)
β ( ((x : A) β C (inl x))
Γ ((y : B) β C (inr y)))
β-universal {A = A} {B} {P} = IsoβEquiv the-iso where
the-iso : Iso _ _


For βsplittingβ a dependent function from the coproduct, we can compose it with either of the constructors to restrict to a function on that factor:

  the-iso .fst f = (Ξ» x β f (inl x)) , (Ξ» x β f (inr x))


Similarly, given a pair of functions, we can do a case split on the coproduct to decide which function to apply:

  the-iso .snd .is-iso.inv (f , g) (inl x) = f x
the-iso .snd .is-iso.inv (f , g) (inr x) = g x

the-iso .snd .is-iso.rinv x = refl
the-iso .snd .is-iso.linv f i (inl x) = f (inl x)
the-iso .snd .is-iso.linv f i (inr x) = f (inr x)


## Transformationsπ

Letβs move away from the abstract nonsense of universal properties for a bit, and cleanse our pallate with some small helper functions for mapping between sum types.

β-map : (A β C) β (B β D) β A β B β C β D
β-map f g (inl a) = inl (f a)
β-map f g (inr b) = inr (g b)

β-mapl : (A β C) β A β B β C β B
β-mapl f = β-map f id

β-mapr : (B β C) β A β B β A β C
β-mapr f = β-map id f


## Decidablityπ

This type has a very similar structure to Dec, so we provide some helpers to convert between the two.

from-dec : Dec A β A β Β¬ A
from-dec (yes a) = inl a
from-dec (no Β¬a) = inr Β¬a

to-dec : A β Β¬ A β Dec A
to-dec (inl  a) = yes a
to-dec (inr Β¬a) = no Β¬a


The proof that these functions are inverses is automatic by computation, and thus it can be shown they are equivalences:

from-dec-is-equiv : {A : Type a} β is-equiv (from-dec {A = A})
from-dec-is-equiv = is-isoβis-equiv (iso to-dec p q) where
p : _
p (inl x)  = refl
p (inr Β¬x) = refl

q : _
q (yes x) = refl
q (no x)  = refl


## Closure under equivalencesπ

Univalence automatically implies that all type formers respect equivalences. However, the proof using univalence is restricted to types of the same universe level. Thus, β-ap: Coproducts respect equivalences in both arguments, across levels.

β-ap : A β B β C β D β (A β C) β (B β D)
β-ap (f , f-eqv) (g , g-eqv) = IsoβEquiv cong where
f-iso = is-equivβis-iso f-eqv
g-iso = is-equivβis-iso g-eqv

cong : Iso _ _
cong .fst = β-map f g

cong .snd .is-iso.inv (inl x) = inl (f-iso .is-iso.inv x)
cong .snd .is-iso.inv (inr x) = inr (g-iso .is-iso.inv x)

cong .snd .is-iso.rinv (inl x) = ap inl (f-iso .is-iso.rinv x)
cong .snd .is-iso.rinv (inr x) = ap inr (g-iso .is-iso.rinv x)

cong .snd .is-iso.linv (inl x) = ap inl (f-iso .is-iso.linv x)
cong .snd .is-iso.linv (inr x) = ap inr (g-iso .is-iso.linv x)

β-apl : A β B β (A β C) β (B β C)
β-apl f = β-ap f (id , id-equiv)

β-apr : B β C β (A β B) β (A β C)
β-apr f = β-ap (id , id-equiv) f


## Algebraic propertiesπ

Considered as an algebraic operator on types, the coproduct satisfies many of the same properties of addition. Specifically, when restricted to finite types, the coproduct is exactly the same as addition.

β-comm : (A β B) β (B β A)
β-comm = IsoβEquiv i where
i : Iso _ _
i .fst (inl x) = inr x
i .fst (inr x) = inl x

i .snd .is-iso.inv (inl x) = inr x
i .snd .is-iso.inv (inr x) = inl x

i .snd .is-iso.rinv (inl x) = refl
i .snd .is-iso.rinv (inr x) = refl
i .snd .is-iso.linv (inl x) = refl
i .snd .is-iso.linv (inr x) = refl

β-assoc : ((A β B) β C) β (A β (B β C))
β-assoc = IsoβEquiv i where
i : Iso _ _
i .fst (inl (inl x)) = inl x
i .fst (inl (inr x)) = inr (inl x)
i .fst (inr x)       = inr (inr x)

i .snd .is-iso.inv (inl x)       = inl (inl x)
i .snd .is-iso.inv (inr (inl x)) = inl (inr x)
i .snd .is-iso.inv (inr (inr x)) = inr x

i .snd .is-iso.rinv (inl x) = refl
i .snd .is-iso.rinv (inr (inl x)) = refl
i .snd .is-iso.rinv (inr (inr x)) = refl

i .snd .is-iso.linv (inl (inl x)) = refl
i .snd .is-iso.linv (inl (inr x)) = refl
i .snd .is-iso.linv (inr x) = refl

β-zeror : (A β β₯) β A
β-zeror .fst (inl x) = x
β-zeror .snd .is-eqv y .centre = inl y , refl
β-zeror .snd .is-eqv y .paths (inl x , p) i = inl (p (~ i)) , Ξ» j β p (~ i β¨ j)

β-zerol : (β₯ β A) β A
β-zerol .fst (inr x) = x
β-zerol .snd .is-eqv y .centre = inr y , refl
β-zerol .snd .is-eqv y .paths (inr x , p) i = inr (p (~ i)) , Ξ» j β p (~ i β¨ j)

β-Γ-distribute : ((A β B) Γ C) β ((A Γ C) β (B Γ C))
β-Γ-distribute = IsoβEquiv i where
i : Iso _ _
i .fst (inl x , y) = inl (x , y)
i .fst (inr x , y) = inr (x , y)
i .snd .is-iso.inv (inl (x , y)) = inl x , y
i .snd .is-iso.inv (inr (x , y)) = inr x , y
i .snd .is-iso.rinv (inl x) = refl
i .snd .is-iso.rinv (inr x) = refl
i .snd .is-iso.linv (inl x , _) = refl
i .snd .is-iso.linv (inr x , _) = refl