open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Universe
open import 1Lab.HLevel.Closure
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.List.Base
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum.Base

open import Meta.Invariant

module Data.Sum.Properties where

As warmup, we have that both constructors are embeddings:

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

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 (lower code)
  decode {x = inr x} {y = inr x₁} code = ap inr (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
  H-Level-⊎ : βˆ€ {n} ⦃ _ : 2 ≀ n ⦄ ⦃ _ : H-Level A n ⦄ ⦃ _ : H-Level B n ⦄ β†’ H-Level (A ⊎ B) n
  H-Level-⊎ {n = suc (suc n)} ⦃ s≀s (s≀s p) ⦄ = hlevel-instance $
    ⊎-is-hlevel _ (hlevel (2 + n)) (hlevel (2 + n))

module _ {β„“} {A : n-Type β„“ 2} where
  _ : is-hlevel (∣ A ∣ ⊎ ∣ A ∣) 5
  _ = hlevel 5

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)

DiscretenessπŸ”—

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

instance
  Discrete-⊎ : ⦃ _ : Discrete A ⦄ ⦃ _ : Discrete B ⦄ β†’ Discrete (A ⊎ B)
  Discrete-⊎ {x = inl x} {inl y} = invmap (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} = invmap (ap inr) inr-inj (x ≑? y)