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