module Data.Sum.Properties where
Properties of sum types🔗
Many useful properties of sum types will fall out of characterising
their path spaces. We start by defining a reflexive family of
codes for paths in A ⊎ B: between elements in the same
component, a code is simply a path in the corresponding type, while
there are no codes between elements in different components.
module ⊎Path {a b} {A : Type a} {B : Type b} where Code : A ⊎ B → A ⊎ B → Type (level-of A ⊔ level-of B) Code (inl x) (inl y) = Lift (level-of B) (x ≡ y) Code (inl x) (inr y) = Lift _ ⊥ Code (inr x) (inl y) = Lift _ ⊥ Code (inr x) (inr y) = Lift (level-of A) (x ≡ y) Code-refl : (x : A ⊎ B) → Code x x Code-refl (inl x) = lift refl Code-refl (inr x) = lift refl
Given a Code for a
path in A ⊎ B, we can turn it into a legitimate path by
applying the corresponding
constructor. 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 y} code = ap inl (lower code) decode {x = inr x} {y = inr y} code = ap inr (lower code)
This lets us show that Code is an identity system, so that we get an
equivalence between codes and paths.
ids : is-identity-system Code Code-refl ids .to-path = decode ids .to-path-over {inl x} {inl y} (lift p) i = lift λ j → p (i ∧ j) ids .to-path-over {inr x} {inr y} (lift p) i = lift λ j → p (i ∧ j) Code≃Path : {x y : A ⊎ B} → (x ≡ y) ≃ Code x y Code≃Path = identity-system-gives-path ids e⁻¹
Injectivity and disjointness of constructors🔗
A first very useful consequence is that the constructors inl and inr are injective and
disjoint:
open ⊎Path inl-inj : {x y : A} → inl {B = B} x ≡ inl y → x ≡ y inl-inj = lower ∘ Code≃Path .fst inr-inj : {A : Type b} {x y : B} → inr {A = A} x ≡ inr y → x ≡ y inr-inj = lower ∘ Code≃Path .fst inl≠inr : {A : Type a} {B : Type b} {x : A} {y : B} → ¬ inl x ≡ inr y inl≠inr = lower ∘ Code≃Path .fst inr≠inl : {A : Type a} {B : Type b} {x : A} {y : B} → ¬ inr x ≡ inl y inr≠inl = lower ∘ Code≃Path .fst
In fact they are even embeddings:
inl-is-embedding : is-embedding (inl {A = A} {B}) inl-is-embedding = cancellable→embedding (Code≃Path ∙e Lift-≃) inr-is-embedding : is-embedding (inr {A = A} {B}) inr-is-embedding = cancellable→embedding (Code≃Path ∙e Lift-≃)
Closure under h-levels🔗
As another consequence, if and are for then so is their coproduct.
We first observe that Code is a family of
which is automatic in every case using instance search:
Code-is-hlevel : {x y : A ⊎ B} {n : Nat} → ⦃ H-Level A (2 + n) ⦄ → ⦃ H-Level B (2 + n) ⦄ → is-hlevel (Code x y) (suc n) Code-is-hlevel {x = inl x} {inl y} {n} = hlevel (suc n) Code-is-hlevel {x = inr x} {inr y} {n} = hlevel (suc n) Code-is-hlevel {x = inl x} {inr y} {n} = hlevel (suc n) Code-is-hlevel {x = inr x} {inl y} {n} = hlevel (suc n)
Thus, so are paths in A ⊎ B, which concludes the
proof.
⊎-is-hlevel : (n : Nat) → ⦃ H-Level A (2 + n) ⦄ → ⦃ H-Level B (2 + n) ⦄ → is-hlevel (A ⊎ B) (2 + n) ⊎-is-hlevel {A = A} {B = B} n x y = Equiv→is-hlevel (1 + n) Code≃Path Code-is-hlevel
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 _
Note that, in general, being a proposition and being contractible is not preserved under
coproducts. Consider the type ⊤ ⊎ ⊤: this is a coproduct of
contractible types (hence propositions) that is not itself a
proposition. 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-⊎ .decide (inl x) (inl y) = invmap (ap inl) inl-inj (x ≡? y) Discrete-⊎ .decide (inl x) (inr y) = no inl≠inr Discrete-⊎ .decide (inr x) (inl y) = no inr≠inl Discrete-⊎ .decide (inr x) (inr y) = invmap (ap inr) inr-inj (x ≡? y)