module 1Lab.HLevel.Retracts where
Closure of h-levels🔗
The homotopy n-types have many closure properties. A trivial example is that they are closed under equivalences, since any property of types is preserved by equivalence (This is the univalence axiom). More interesting is that they are closed under retractions:
Retractions🔗
The first base case is to show that retracts of
contractible types are contractible. We say that
is a retract of
if there is a map
admitting a right-inverse. This
means that
is the retraction (the left inverse). The proof is a calculation:
retract→is-contr : (f : A → B) (g : B → A) → is-left-inverse f g → is-contr A → is-contr B retract→is-contr f g h isC .centre = f (isC .centre) retract→is-contr f g h isC .paths x = f (isC .centre) ≡⟨ ap f (isC .paths _) ⟩≡ f (g x) ≡⟨ h _ ⟩≡ x ∎
We must also show that retracts of propositions are propositions:
retract→is-prop : (f : A → B) (g : B → A) → is-left-inverse f g → is-prop A → is-prop B retract→is-prop f g h propA x y = x ≡⟨ sym (h _) ⟩≡ f (g x) ≡⟨ ap f (propA _ _) ⟩≡ f (g y) ≡⟨ h _ ⟩≡ y ∎
Now we can extend this to all h-levels by induction:
retract→is-hlevel : (n : Nat) (f : A → B) (g : B → A) → is-left-inverse f g → is-hlevel A n → is-hlevel B n retract→is-hlevel 0 = retract→is-contr retract→is-hlevel 1 = retract→is-prop
For the base case, we already have the proofs we’re after. For the
inductive case, a function g x ≡ g y → x ≡ y is
constructed, which is a left inverse to the function ap g.
Then, since (g x) ≡ (g y) is a homotopy (n+1)-type, we
conclude that so is x ≡ y.
retract→is-hlevel (suc (suc n)) f g h hlevel x y = retract→is-hlevel (suc n) sect (ap g) inv (hlevel (g x) (g y)) where sect : g x ≡ g y → x ≡ y sect path = x ≡⟨ sym (h _) ⟩≡ f (g x) ≡⟨ ap f path ⟩≡ f (g y) ≡⟨ h _ ⟩≡ y ∎
The left inverse is constructed out of ap and the given homotopy.
inv : is-left-inverse sect (ap g) inv path = sym (h x) ∙ ap f (ap g path) ∙ h y ∙ refl ≡⟨ ap (λ e → sym (h _) ∙ _ ∙ e) (∙-id-r (h _)) ⟩≡ sym (h x) ∙ ap f (ap g path) ∙ h y ≡⟨ ap₂ _∙_ refl (sym (homotopy-natural h _)) ⟩≡ sym (h x) ∙ h x ∙ path ≡⟨ ∙-assoc _ _ _ ⟩≡ (sym (h x) ∙ h x) ∙ path ≡⟨ ap₂ _∙_ (∙-inv-l (h x)) refl ⟩≡ refl ∙ path ≡⟨ ∙-id-l path ⟩≡ path ∎
The proof that this function does invert ap g
on the left is boring, but it consists mostly of symbol pushing. The
only non-trivial step, and the key to the proof, is the theorem that homotopies are natural
transformations: We can flip ap f (ap g path) and
h y to get a pair of paths that annihilates on the left,
and path on the right.
Equivalences🔗
It follows, without a use of univalence, that h-levels are closed under isomorphisms and equivalences:
iso→is-hlevel : (n : Nat) (f : A → B) → is-iso f → is-hlevel A n → is-hlevel B n iso→is-hlevel n f is-iso = retract→is-hlevel n f (is-iso .is-iso.inv) (is-iso .is-iso.rinv) equiv→is-hlevel : (n : Nat) (f : A → B) → is-equiv f → is-hlevel A n → is-hlevel B n equiv→is-hlevel n f eqv = iso→is-hlevel n f (is-equiv→is-iso eqv) is-hlevel≃ : (n : Nat) → (B ≃ A) → is-hlevel A n → is-hlevel B n is-hlevel≃ n f = iso→is-hlevel n (Equiv.from f) (iso (Equiv.to f) (Equiv.η f) (Equiv.ε f)) Iso→is-hlevel : (n : Nat) → Iso B A → is-hlevel A n → is-hlevel B n Iso→is-hlevel n (f , isic) = iso→is-hlevel n (isic .is-iso.inv) $ iso f (isic .is-iso.linv) (isic .is-iso.rinv)
Functions into n-types🔗
Since h-levels are closed under retracts, The type of functions into a homotopy n-type is itself a homotopy n-type.
Π-is-hlevel : ∀ {a b} {A : Type a} {B : A → Type b} → (n : Nat) (Bhl : (x : A) → is-hlevel (B x) n) → is-hlevel ((x : A) → B x) n Π-is-hlevel 0 bhl = contr (λ x → bhl _ .centre) λ x i a → bhl _ .paths (x a) i Π-is-hlevel 1 bhl f g i a = bhl a (f a) (g a) i Π-is-hlevel (suc (suc n)) bhl f g = retract→is-hlevel (suc n) funext happly (λ x → refl) (Π-is-hlevel (suc n) λ x → bhl x (f x) (g x))
Π-is-hlevel′ : ∀ {a b} {A : Type a} {B : A → Type b} → (n : Nat) (Bhl : (x : A) → is-hlevel (B x) n) → is-hlevel ({x : A} → B x) n Π-is-hlevel′ n bhl = retract→is-hlevel n (λ f {x} → f x) (λ f x → f) (λ _ → refl) (Π-is-hlevel n bhl) Π-is-hlevel² : ∀ {a b c} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c} → (n : Nat) (Bhl : (x : A) (y : B x) → is-hlevel (C x y) n) → is-hlevel (∀ x y → C x y) n Π-is-hlevel² n w = Π-is-hlevel n λ _ → Π-is-hlevel n (w _) Π-is-hlevel³ : ∀ {a b c d} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c} {D : ∀ a b → C a b → Type d} → (n : Nat) (Bhl : (x : A) (y : B x) (z : C x y) → is-hlevel (D x y z) n) → is-hlevel (∀ x y z → D x y z) n Π-is-hlevel³ n w = Π-is-hlevel n λ _ → Π-is-hlevel² n (w _)
By taking B to be a type rather than a family, we get
that A → B also inherits the h-level of B.
fun-is-hlevel : ∀ {a b} {A : Type a} {B : Type b} → (n : Nat) → is-hlevel B n → is-hlevel (A → B) n fun-is-hlevel n hl = Π-is-hlevel n (λ _ → hl)
Sums of n-types🔗
A similar argument, using the fact that paths of pairs are pairs of paths, shows that dependent sums are also closed under h-levels.
Σ-is-hlevel : {A : Type ℓ} {B : A → Type ℓ'} (n : Nat) → is-hlevel A n → ((x : A) → is-hlevel (B x) n) → is-hlevel (Σ A B) n Σ-is-hlevel 0 acontr bcontr = contr (acontr .centre , bcontr _ .centre) λ x → Σ-pathp (acontr .paths _) (is-prop→pathp (λ _ → is-contr→is-prop (bcontr _)) _ _) Σ-is-hlevel 1 aprop bprop (a , b) (a' , b') i = (aprop a a' i) , (is-prop→pathp (λ i → bprop (aprop a a' i)) b b' i) Σ-is-hlevel {B = B} (suc (suc n)) h1 h2 x y = iso→is-hlevel (suc n) (is-iso.inverse (Σ-path-iso .snd) .is-iso.inv) (Σ-path-iso .snd) (Σ-is-hlevel (suc n) (h1 (fst x) (fst y)) λ x → h2 _ _ _)
Similarly for dependent products and functions, there is a
non-dependent version of Σ-is-hlevel that expresses closure of
h-levels under _×_.
×-is-hlevel : ∀ {a b} {A : Type a} {B : Type b} → (n : Nat) → is-hlevel A n → is-hlevel B n → is-hlevel (A × B) n ×-is-hlevel n ahl bhl = Σ-is-hlevel n ahl (λ _ → bhl)
Similarly, Lift does not induce a change of h-levels, i.e. if is an -type in a universe , then it’s also an -type in any successor universe:
Lift-is-hlevel : ∀ {a b} {A : Type a} → (n : Nat) → is-hlevel A n → is-hlevel (Lift b A) n Lift-is-hlevel n a-hl = retract→is-hlevel n lift Lift.lower (λ _ → refl) a-hl
Automation🔗
For the common case of proving that a composite type built out of pieces with a known h-level has that same h-level, we can apply the helpers above very uniformly. So uniformly, in fact, that Agda’s instance resolution mechanism can do it for us. However, since is-hlevel is a recursive definition which unfolds depending on the level, we must introduce a record wrapper around this type which prevents recursion. Otherwise we could not expect Agda to find instances in scope.
record H-Level {ℓ} (T : Type ℓ) (n : Nat) : Type ℓ where constructor hlevel-instance field has-hlevel : is-hlevel T n
The canonical entry point for the search is hlevel, which turns an instance argument of H-Level to an actual usable witness. Note that the parameter is explicit: We can not expect Agda to recover from the expected type of the application.
hlevel : ∀ {ℓ} {T : Type ℓ} n ⦃ x : H-Level T n ⦄ → is-hlevel T n hlevel n ⦃ x ⦄ = H-Level.has-hlevel x private variable ℓ′ : Level S T : Type ℓ module _ where open H-Level H-Level-is-prop : ∀ {n} → is-prop (H-Level T n) H-Level-is-prop {n = n} x y i .has-hlevel = is-hlevel-is-prop n (x .has-hlevel) (y .has-hlevel) i
Because of the way we set up our search, the “leaves” in the instance search must support offsetting the index by any positive number: Rather than defining an instance saying that e.g. has h-level 2, we define an instance saying it has h-level , for any choice of . This is done using the basic-instance helper:
basic-instance : ∀ {ℓ} {T : Type ℓ} n → is-hlevel T n → ∀ {k} → H-Level T (n + k) basic-instance {T = T} n hl {k} = subst (H-Level T) (+-comm n k) (hlevel-instance (is-hlevel-+ n k hl)) where +-comm : ∀ n k → k + n ≡ n + k +-comm zero k = go k where go : ∀ k → k + 0 ≡ k go zero = refl go (suc x) = ap suc (go x) +-comm (suc n) k = go n k ∙ ap suc (+-comm n k) where go : ∀ n k → k + suc n ≡ suc (k + n) go n zero = refl go n (suc k) = ap suc (go n k) prop-instance : ∀ {ℓ} {T : Type ℓ} → is-prop T → ∀ {k} → H-Level T (suc k) prop-instance {T = T} hl = hlevel-instance (is-prop→is-hlevel-suc hl)
We then have a family of instances for solving compound types, e.g. function types, -types, path types, lifts, etc.
instance H-Level-pi : ∀ {n} {S : T → Type ℓ} → ⦃ ∀ {x} → H-Level (S x) n ⦄ → H-Level (∀ x → S x) n H-Level-pi {n = n} .H-Level.has-hlevel = Π-is-hlevel n λ _ → hlevel n H-Level-⊤ : ∀ {n} → H-Level ⊤ n H-Level-⊤ {n = zero} = hlevel-instance (contr tt (λ x i → tt)) H-Level-⊤ {n = suc n} = prop-instance λ x y i → tt H-Level-⊥ : ∀ {n} → H-Level ⊥ (suc n) H-Level-⊥ {n = n} = prop-instance λ x y → absurd x H-Level-pi′ : ∀ {n} {S : T → Type ℓ} → ⦃ ∀ {x} → H-Level (S x) n ⦄ → H-Level (∀ {x} → S x) n H-Level-pi′ {n = n} .H-Level.has-hlevel = Π-is-hlevel′ n λ _ → hlevel n H-Level-sigma : ∀ {n} {S : T → Type ℓ} → ⦃ H-Level T n ⦄ → ⦃ ∀ {x} → H-Level (S x) n ⦄ → H-Level (Σ T S) n H-Level-sigma {n = n} .H-Level.has-hlevel = Σ-is-hlevel n (hlevel n) λ _ → hlevel n H-Level-path′ : ∀ {n} ⦃ s : H-Level S (suc n) ⦄ {x y} → H-Level (Path S x y) n H-Level-path′ {n = n} .H-Level.has-hlevel = Path-is-hlevel' n (hlevel (suc n)) _ _ H-Level-Lift : ∀ {n} ⦃ s : H-Level T n ⦄ → H-Level (Lift ℓ T) n H-Level-Lift {n = n} .H-Level.has-hlevel = Lift-is-hlevel n (hlevel n) H-Level-is-contr : ∀ {n} {ℓ} {T : Type ℓ} → H-Level (is-contr T) (suc n) H-Level-is-contr = prop-instance is-contr-is-prop