module 1Lab.HLevel.Closure where
Closure of h-levels🔗
When showing that a given type is a homotopy -type, it’s often possible to reason syntactically about the type formers which were used in the construction of This is fundamentally because the are closed under a variety of type-forming operations, and that fact boils down to the fact that, in a homotopy type theory, the structure of identity types tends to be “self-similar” — for example, paths between pairs are pairs of paths.
Split surjections and retractions🔗
The fundamental result that we will piggy-back to derive the closure of under various operations is that contractible types are closed under split surjections. Unfolding this, it says that if we have a map and a section assigning fibres of over each then is contractible whenever is.
The proof is a short calculation:
split-surjection→is-contr : (f : A → B) (s : (b : B) → fibre f b) → is-contr A → is-contr B split-surjection→is-contr f s c .centre = f (c .centre) split-surjection→is-contr f s c .paths x = f (c .centre) ≡⟨ ap f (c .paths _) ⟩≡ f (s x .fst) ≡⟨ s x .snd ⟩≡ x ∎
Usually, the data of a split surjection is unpacked to talk about retractions instead. That is, instead of talking about a section of fibres, we unpack the components to mention the inverse map and the proof that
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 ∎
Recalling that our hierarchy of has two base cases, if we are to show that all h-levels are closed under retractions, we should also repeat the argument above for propositions. This turns out to be no biggie, so that there is no impediment to starting the inductive proof.
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 ∎ 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
In the inductive case, we show that a retraction induces retractions between path spaces: the map is a split surjection. The construction simply whiskers the proof with paths that cancel
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 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 behave like 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.
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) (∙-idr (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₂ _∙_ (∙-invl (h x)) refl ⟩≡ refl ∙ path ≡⟨ ∙-idl path ⟩≡ path ∎
Isomorphisms and equivalences🔗
Even though we know that univalence implies that are closed under equivalences, this does not apply to types in different universe levels. However, the construction above does, since every equivalence, having a two-sided inverse, is a split surjection.
iso→is-hlevel : (n : Nat) (f : A → B) → is-iso f → is-hlevel A n → is-hlevel B n iso→is-hlevel n f im = retract→is-hlevel n f g h where open is-iso im renaming (inv to g ; rinv to h) Iso→is-hlevel : (n : Nat) → Iso B A → is-hlevel A n → is-hlevel B n Iso→is-hlevel n (f , im) = retract→is-hlevel n g f h where open is-iso im renaming (inv to g ; linv to h) 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) Equiv→is-hlevel : (n : Nat) → (B ≃ A) → is-hlevel A n → is-hlevel B n Equiv→is-hlevel n f = equiv→is-hlevel n _ (Equiv.inverse f .snd)
Functions into n-types🔗
We can now prove that the are closed under all type formers whose identity types are “self-similar”. While we have to handle the base cases ourselves, closure under retracts can take care of the inductive cases. Function extensionality implies that an identity between functions is a function into identities:
Π-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 = record { paths = λ 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} {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 _) Π-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 the codomain to be a constant family, we obtain that the are an exponential ideal: is an if is.
fun-is-hlevel : ∀ n → 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 between pairs are pairs of paths,
shows that dependent sums are also closed under h-levels.
Σ-is-hlevel : {B : A → Type ℓ'} (n : Nat) → is-hlevel A n → (∀ x → is-hlevel (B x) n) → is-hlevel (Σ A B) n Σ-is-hlevel 0 acontr bcontr = record { centre = acontr .centre , bcontr _ .centre ; paths = λ 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 , p) (y , q) = iso→is-hlevel (suc n) _ (Σ-path-iso .snd) $ Σ-is-hlevel (suc n) (h1 x y) λ x → h2 y (subst B x p) q
Analogous to the case of dependent products and functions, a non-dependent sum is a product.
×-is-hlevel : ∀ n → 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
in a universe
then it’s also an
in any successor universe:
opaque Lift-is-hlevel : ∀ n → is-hlevel A n → is-hlevel (Lift ℓ' A) n Lift-is-hlevel n a-hl = retract→is-hlevel n lift Lift.lower (λ _ → refl) a-hl
Lift-is-hlevel' : ∀ n → is-hlevel (Lift ℓ' A) n → is-hlevel A n Lift-is-hlevel' n lift-hl = retract→is-hlevel n Lift.lower lift (λ _ → refl) lift-hl
Finally, we’ll show that the fibres of a function between
are themselves
fibre-is-hlevel : ∀ n → is-hlevel A n → is-hlevel B n → (f : A → B) → ∀ b → is-hlevel (fibre f b) n fibre-is-hlevel n Ah Bh f b = Σ-is-hlevel n Ah λ _ → Path-is-hlevel n Bh
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 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, path types, lifts, etc.
instance opaque 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-PathP : ∀ {n} {S : I → Type ℓ} ⦃ s : H-Level (S i1) (suc n) ⦄ {x y} → H-Level (PathP S x y) n H-Level-PathP {n = n} .H-Level.has-hlevel = PathP-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 H-Level-is-equiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n} → H-Level (is-equiv f) (suc n) H-Level-is-equiv = prop-instance (is-equiv-is-prop _)