open import 1Lab.Reflection.HLevel open import 1Lab.HLevel.Retracts open import 1Lab.HLevel.Universe open import 1Lab.HLevel open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type open import Data.List.Base open import Data.Sum.Base 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 β-disjoint : {A : Type a} {B : Type b} {x : A} {y : B} β Β¬ inl x β‘ inr y β-disjoint path = subst (Ξ» { (inl x) β β€ ; (inr x) β β₯ }) path tt
Closure under h-levelsπ
If
and
are
-types,
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 (β-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} β (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 = 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 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)