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) (∙-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 ∎
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.
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 between 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
Likewise, if the Lift of
is an
-type,
then
must also be an n-type.
Lift-is-hlevel' : ∀ {a b} {A : Type a} → (n : Nat) → is-hlevel (Lift b A) n → is-hlevel A n Lift-is-hlevel' n lift-hl = retract→is-hlevel n Lift.lower lift (λ _ → refl) lift-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-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