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

module Data.Sum 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 1 _⊎_

data _⊎_ {a b} (A : Type a) (B : Type b) : Type (a βŠ” b) where
  inl : A β†’ A ⊎ B
  inr : B β†’ A ⊎ B

As warmup, we have that both constructors are embeddings:

inl-inj : {B : Type b} {x y : A} β†’ inl {B = B} x ≑ inl y β†’ x ≑ y
inl-inj {A = A} {x = x} path = ap f path where
  f : A ⊎ B β†’ A
  f (inl x) = x
  f (inr _) = x

inr-inj : {A : Type b} {x y : B} β†’ inr {A = A} x ≑ inr y β†’ x ≑ y
inr-inj {B = B} {x = x} path = ap f path where
  f : A ⊎ B β†’ B
  f (inl _) = x
  f (inr x) = x

⊎-disjoint : {A : Type a} {B : Type b} {x : A} {y : B} β†’ inl x ≑ inr y β†’ βŠ₯
⊎-disjoint path = subst (Ξ» { (inl x) β†’ ⊀ ; (inr x) β†’ βŠ₯ }) path tt

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

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 h-levelsπŸ”—

If AA and BB are nn-types, for nβ‰₯2n \ge 2, then so is their coproduct. The way we prove this is by characterising the entire path space of A ⊎ B in terms of the path spaces for A and B, using a recursive definition:

module ⊎Path where
  Code : A ⊎ B β†’ A ⊎ B β†’ Type (level-of A βŠ” level-of B)
  Code {B = B} (inl x) (inl y) = Lift (level-of B) (x ≑ y)
  Code (inl x) (inr y) = Lift _ βŠ₯
  Code (inr x) (inl y) = Lift _ βŠ₯
  Code {A = A} (inr x) (inr y) = Lift (level-of A) (x ≑ y)

Given a Code for a path in A ⊎ B, we can turn it into a legitimate path. Agda automatically lets us ignore the cases where the Code computes to the empty type.

  decode : {x y : A ⊎ B} β†’ Code x y β†’ x ≑ y
  decode {x = inl x} {y = inl x₁} code = ap inl (Lift.lower code)
  decode {x = inr x} {y = inr x₁} code = ap inr (Lift.lower code)

In the inverse direction, we have a procedure for turning paths into codes:

  encode : {x y : A ⊎ B} β†’ x ≑ y β†’ Code x y
  encode {x = inl x} {y = inl y} path = lift (inl-inj path)
  encode {x = inl x} {y = inr y} path = absurd (⊎-disjoint path)
  encode {x = inr x} {y = inl y} path = absurd (⊎-disjoint (sym path))
  encode {x = inr x} {y = inr y} path = lift (inr-inj path)

Now we must establish that encode and decode are inverses. In the one direction, we can use path induction:

  decode-encode : {x y : A ⊎ B} (p : x ≑ y) β†’ decode (encode p) ≑ p
  decode-encode = J (Ξ» _ p β†’ decode (encode p) ≑ p) d-e-refl where
    d-e-refl : {x : A ⊎ B} β†’ decode (encode (Ξ» i β†’ x)) ≑ (Ξ» i β†’ x)
    d-e-refl {x = inl x} = refl
    d-e-refl {x = inr x} = refl

In the other direction, the proof is by case analysis, and everything computes wonderfully to make the right-hand sides fillable by refl:

  encode-decode : {x y : A ⊎ B} (p : Code x y) β†’ encode (decode p) ≑ p
  encode-decode {x = inl x} {y = inl y} p = refl
  encode-decode {x = inr x} {y = inr y} p = refl

Thus, we have an equivalence between codes for paths in A ⊎ B and actual paths A ⊎ B. Since Code has a nice computational structure, we can establish its h-level by induction:

  Code≃Path : {x y : A ⊎ B} β†’ Code x y ≃ (x ≑ y)
  Code≃Path = Isoβ†’Equiv (decode , iso encode decode-encode encode-decode)

open ⊎Path

Code-is-hlevel : {x y : A ⊎ B} {n : Nat}
               β†’ is-hlevel A (2 + n)
               β†’ is-hlevel B (2 + n)
               β†’ is-hlevel (Code x y) (suc n)
Code-is-hlevel {x = inl x} {inl y} {n} ahl bhl =
  Lift-is-hlevel (suc n) (ahl x y)
Code-is-hlevel {x = inr x} {inr y} {n} ahl bhl =
  Lift-is-hlevel (suc n) (bhl x y)

In the two cases where x and y match, we can use the fact that Lift preserves h-levels and the assumption that A (or B) have the given h-level.

Code-is-hlevel {x = inl x} {inr y} {n} ahl bhl =
  Lift-is-hlevel (suc n) (is-prop→is-hlevel-suc λ x → absurd x)
Code-is-hlevel {x = inr x} {inl y} {n} ahl bhl =
  Lift-is-hlevel (suc n) (is-prop→is-hlevel-suc λ x → absurd x)

In the mismatched cases, we use the fact that propositions have any successor h-level to prove that βŠ₯ is also at the same h-level as A and B. Thus, we have:

⊎-is-hlevel : (n : Nat)
            β†’ is-hlevel A (2 + n)
            β†’ is-hlevel B (2 + n)
            β†’ is-hlevel (A ⊎ B) (2 + n)
⊎-is-hlevel n ahl bhl x y = is-hlevel≃ (1 + n) Code≃Path (Code-is-hlevel ahl bhl)

Note that, in general, being a proposition and being contractible are not preserved under coproducts. Consider the case where (A, a) and (B, b) are both contractible (this generalises to propositions): Then their coproduct has two distinct points, inΒ­l a and inr b. However, the coproduct of disjoint propositions is a proposition:

disjoint-⊎-is-prop
  : is-prop A β†’ is-prop B β†’ (A Γ— B β†’ βŠ₯)
  β†’ is-prop (A ⊎ B)
disjoint-⊎-is-prop Ap Bp notab (inl x) (inl y) = ap inl (Ap x y)
disjoint-⊎-is-prop Ap Bp notab (inl x) (inr y) = absurd (notab (x , y))
disjoint-⊎-is-prop Ap Bp notab (inr x) (inl y) = absurd (notab (y , x))
disjoint-⊎-is-prop Ap Bp notab (inr x) (inr y) = ap inr (Bp x y)

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 (inl x) = inl (f x)
  cong .fst (inr x) = inr (g x)

  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