module Data.Sum.Properties where

As warmup, we have that both constructors are embeddings:

inl-inj : {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

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

inrβ‰ inl : {A : Type a} {B : Type b} {x : A} {y : B} β†’ Β¬ inr x ≑ inl y
inr≠inl path = inl≠inr (sym path)

Closure under h-levelsπŸ”—

If and are for 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 (inl≠inr path)
  encode {x = inr x} {y = inl y} path = absurd (inr≠inl 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} β†’ (x ≑ y) ≃ Code x y
  Code≃Path = Isoβ†’Equiv (encode , iso decode encode-decode decode-encode)
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 =
  Equivβ†’is-hlevel (1 + n) Code≃Path (Code-is-hlevel ahl bhl)

instance
  hlevel-decomp-⊎ : hlevel-decomposition (A ⊎ B)
  hlevel-decomp-⊎ = decomp (quote ⊎-is-hlevel)
    (`level-minus 2 ∷ `search ∷ `search ∷ [])

Note that, in general, being a proposition and 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, inl 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)

DecidabilityπŸ”—

If A and B are decidable, then so is A ⊎ B.

instance
  Dec-⊎ : ⦃ _ : Dec A ⦄ ⦃ _ : Dec B ⦄ β†’ Dec (A ⊎ B)
  Dec-⊎ ⦃ yes A ⦄ = yes (inl A)
  Dec-⊎ ⦃ no Β¬A ⦄ ⦃ yes B ⦄ = yes (inr B)
  Dec-⊎ ⦃ no Β¬A ⦄ ⦃ no Β¬B ⦄ = no Ξ» where
    (inl A) β†’ Β¬A A
    (inr B) β†’ Β¬B B

  Discrete-⊎ : ⦃ _ : Discrete A ⦄ ⦃ _ : Discrete B ⦄ β†’ Discrete (A ⊎ B)
  Discrete-⊎ {x = inl x} {inl y} = Dec-map (ap inl) inl-inj (x ≑? y)
  Discrete-⊎ {x = inl x} {inr y} = no inlβ‰ inr
  Discrete-⊎ {x = inr x} {inl y} = no inrβ‰ inl
  Discrete-⊎ {x = inr x} {inr y} = Dec-map (ap inr) inr-inj (x ≑? y)