module Homotopy.Truncation where
General truncations🔗
Inspired by the equivalence between loop spaces and maps out of spheres, although not using it directly, we can characterise h-levels in terms of maps of spheres, too. The idea is that, since a map is equivalently some loop in 1, we can characterise the trivial loops as the constant functions Correspondingly, if every function is trivial, this means that all in are trivial, so that is
We refer to a trivialisation of a map as being a “hubs-and-spokes” construction. Geometrically, a trivial loop can be understood as a map from the disc rather than the where the is the type generated by attaching a new point to the sphere (the “hub”), and paths connecting the hub to each point along the sphere (the “spokes”). The resulting type is contractible, whence every function out of it is constant.
hlevel→hubs-and-spokes : ∀ {ℓ} {A : Type ℓ} (n : Nat) → is-hlevel A (suc n) → (sph : Sⁿ n .fst → A) → Σ[ hub ∈ A ] (∀ x → sph x ≡ hub) hubs-and-spokes→hlevel : ∀ {ℓ} {A : Type ℓ} (n : Nat) → ((sph : Sⁿ n .fst → A) → Σ[ hub ∈ A ] (∀ x → sph x ≡ hub)) → is-hlevel A (suc n)
hlevel→hubs-and-spokes 0 prop sph = sph north , λ x → prop (sph x) (sph north) hlevel→hubs-and-spokes {A = A} (suc n) h = helper λ x y → hlevel→hubs-and-spokes n (h x y) where helper : ((a b : A) → (sph : Sⁿ⁻¹ (1 + n) → a ≡ b) → Σ _ λ hub → ∀ x → sph x ≡ hub) → (sph : Sⁿ⁻¹ (2 + n) → A) → Σ _ λ hub → ∀ x → sph x ≡ hub helper h f = f north , sym ∘ r where r : (x : Sⁿ⁻¹ (2 + n)) → f north ≡ f x r north = refl r south = h (f north) (f south) (λ x i → f (merid x i)) .fst r (merid x i) j = hcomp (∂ i ∨ ∂ j) λ where k (i = i0) → f north k (i = i1) → h (f north) (f south) (λ x i → f (merid x i)) .snd x k j k (j = i0) → f north k (j = i1) → f (merid x i) k (k = i0) → f (merid x (i ∧ j)) hubs-and-spokes→hlevel {A = A} zero spheres x y = spheres go .snd north ∙ sym (spheres go .snd south) where go : Sⁿ⁻¹ 1 → A go north = x go south = y hubs-and-spokes→hlevel {A = A} (suc n) spheres x y = hubs-and-spokes→hlevel n $ helper spheres x y where helper : ((sph : Sⁿ⁻¹ (2 + n) → A) → Σ _ λ hub → ∀ x → sph x ≡ hub) → ∀ a b → (sph : Sⁿ⁻¹ (1 + n) → a ≡ b) → Σ _ λ hub → ∀ x → sph x ≡ hub helper h x y f = _ , r where f' : Sⁿ⁻¹ (2 + n) → A f' north = x f' south = y f' (merid u i) = f u i r : (s : Sⁿ⁻¹ (1 + n)) → f s ≡ h f' .snd north ∙ sym (h f' .snd south) r s i j = hcomp (∂ i ∨ ∂ j) λ where k (k = i0) → h f' .snd north (~ i ∨ j) k (i = i0) → h f' .snd (merid s j) (~ k) k (i = i1) → hfill (∂ j) k λ where l (j = i0) → x l (j = i1) → h f' .snd south (~ l) l (l = i0) → h f' .snd north j k (j = i0) → h f' .snd north (~ i ∧ ~ k) k (j = i1) → h f' .snd south (~ k)
Using this idea, we can define a general
type, as a joint generalisation of the propositional and set truncations. While we can not
directly build a type with a constructor saying the type is
what we can do is freely generate hub
s and spokes
for any
drawn on the
of
The result is the universal
admitting a map from
data n-Tr {ℓ} (A : Type ℓ) n : Type ℓ where inc : A → n-Tr A n hub : (r : Sⁿ⁻¹ n → n-Tr A n) → n-Tr A n spokes : (r : Sⁿ⁻¹ n → n-Tr A n) → ∀ x → r x ≡ hub r
For both proving that the has the right h-level, and proving that one can eliminate from it to we use the characterisations of truncation in terms of hubs-and-spokes.
abstract n-Tr-is-hlevel : ∀ {ℓ} {A : Type ℓ} n → is-hlevel (n-Tr A (suc n)) (suc n) n-Tr-is-hlevel n = hubs-and-spokes→hlevel n λ sph → hub sph , spokes sph instance H-Level-n-Tr : ∀ {ℓ} {A : Type ℓ} {n k} ⦃ _ : suc n ≤ k ⦄ → H-Level (n-Tr A (suc n)) k H-Level-n-Tr {k = _} ⦃ p ⦄ = hlevel-instance $ is-hlevel-le _ _ p (n-Tr-is-hlevel _) n-Tr-elim : ∀ {ℓ ℓ'} {A : Type ℓ} {n} → (P : n-Tr A (suc n) → Type ℓ') → (∀ x → is-hlevel (P x) (suc n)) → (∀ x → P (inc x)) → ∀ x → P x n-Tr-elim {A = A} {n} P ptrunc pbase = go where module _ (r : Sⁿ n .fst → n-Tr A (1 + n)) (w : (x : Sⁿ n .fst) → P (r x)) where circle : Sⁿ⁻¹ (1 + n) → P (hub r) circle x = subst P (spokes r x) (w x) hub' = hlevel→hubs-and-spokes n (ptrunc (hub r)) circle .fst spokes' : ∀ x → PathP (λ i → P (spokes r x i)) (w x) hub' spokes' x = to-pathp $ hlevel→hubs-and-spokes n (ptrunc (hub r)) circle .snd x go : ∀ x → P x go (inc x) = pbase x go (hub r) = hub' r (λ x → go (r x)) go (spokes r x i) = spokes' r (λ x → go (r x)) x i
instance Inductive-n-Tr : ∀ {ℓ ℓ' ℓm} {A : Type ℓ} {n} {P : n-Tr A (suc n) → Type ℓ'} ⦃ i : Inductive (∀ x → P (inc x)) ℓm ⦄ → ⦃ _ : ∀ {x} → H-Level (P x) (suc n) ⦄ → Inductive (∀ x → P x) ℓm Inductive-n-Tr ⦃ i ⦄ = record { from = λ f → n-Tr-elim _ (λ x → hlevel _) (i .Inductive.from f) } n-Tr-elim! : ∀ {ℓ ℓ'} {A : Type ℓ} {n} → (P : n-Tr A (suc n) → Type ℓ') → ⦃ _ : ∀ {x} → H-Level (P x) (suc n) ⦄ → (∀ x → P (inc x)) → ∀ x → P x n-Tr-elim! P f = n-Tr-elim P (λ x → hlevel _) f n-Tr-rec! : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} → ⦃ hl : H-Level B (suc n) ⦄ → (A → B) → n-Tr A (suc n) → B n-Tr-rec! = n-Tr-elim (λ _ → _) (λ _ → hlevel _) n-Tr-map : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} → (A → B) → n-Tr A (suc n) → n-Tr B (suc n) n-Tr-map f = n-Tr-rec! (inc ∘ f) n-Tr-ap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} → (e : A ≃ B) → n-Tr A (suc n) ≃ n-Tr B (suc n) n-Tr-ap e .fst = n-Tr-map (e .fst) n-Tr-ap e .snd = is-iso→is-equiv λ where .is-iso.from → n-Tr-map (Equiv.from e) .is-iso.rinv → elim! λ _ → ap inc (Equiv.ε e _) .is-iso.linv → elim! λ _ → ap inc (Equiv.η e _)
As a simpler case of n-Tr-elim
, we have the
recursion principle, where the type we are eliminating into is
constant.
n-Tr-rec : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} → is-hlevel B (suc n) → (A → B) → n-Tr A (suc n) → B n-Tr-rec hl = n-Tr-elim (λ _ → _) (λ _ → hl)
An initial application of the induction principle for of is characterising its path spaces, at least for the inclusions of points from Identifications between (the images of) points in in the are equivalently identifications in
n-Tr-path-equiv : ∀ {ℓ} {A : Type ℓ} {n} {x y : A} → Path (n-Tr A (2 + n)) (inc x) (inc y) ≃ n-Tr (x ≡ y) (suc n) n-Tr-path-equiv {A = A} {n} {x = x} {y} = Iso→Equiv isom where
The proof is an application of the encode-decode method. We would like to characterise the space
so we will, for every define a type family where the fibre of over should be However, the induction principle for only allows us to map into while itself is not an for any We salvage our definition by instead mapping into which is a
code : (x : A) (y' : n-Tr A (2 + n)) → n-Type _ (suc n) code x = n-Tr-rec! λ y' → el! (n-Tr (Path A x y') (suc n))
The rest of the proof boils down to applications of path induction
and the induction
principle for
encode' : ∀ x y → inc x ≡ y → ∣ code x y ∣ encode' x _ = J (λ y _ → ∣ code x y ∣) (inc refl) decode' : ∀ x y → ∣ code x y ∣ → inc x ≡ y decode' = elim! λ x y → ap inc rinv : ∀ x y → is-right-inverse (decode' x y) (encode' x y) rinv = elim! λ x y x=y → ap n-Tr.inc (subst-path-right _ _ ∙ ∙-idl _) linv : ∀ x y → is-left-inverse (decode' x y) (encode' x y) linv x _ = J (λ y p → decode' x y (encode' x y p) ≡ p) (ap (decode' x (inc x)) (transport-refl (inc refl)) ∙ refl) isom : Iso (inc x ≡ inc y) (n-Tr (x ≡ y) (suc n)) isom = encode' _ (inc _) , iso (decode' _ (inc _)) (rinv _ (inc _)) (linv _ (inc _))
We can also phrase the recursion principle as an equivalence between functions out of and functions out of as long as the codomain is appropriately truncated.
n-Tr-univ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} n → is-hlevel B (suc n) → (n-Tr A (suc n) → B) ≃ (A → B) n-Tr-univ n b-hl .fst f = f ∘ inc n-Tr-univ n b-hl .snd = is-iso→is-equiv λ where .is-iso.from f → n-Tr-rec b-hl f .is-iso.rinv f → refl .is-iso.linv f → funext $ n-Tr-elim _ (λ x → Path-is-hlevel (suc n) b-hl) λ _ → refl
Closure properties🔗
We can prove that commutes with (binary) products by pattern-matching. The benefit of writing out all the clauses is that we end up with much shorter neutral forms; and, while there are quite a few, they are very simple.
n-Tr-product : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} → n-Tr (A × B) (suc n) ≃ (n-Tr A (suc n) × n-Tr B (suc n)) n-Tr-product {A = A} {B} {n} = distrib , distrib-is-equiv where distrib : n-Tr (A × B) (suc n) → n-Tr A (suc n) × n-Tr B (suc n) distrib (inc (x , y)) = inc x , inc y distrib (hub r) .fst = hub λ s → distrib (r s) .fst distrib (hub r) .snd = hub λ s → distrib (r s) .snd distrib (spokes r x i) .fst = spokes (λ s → distrib (r s) .fst) x i distrib (spokes r x i) .snd = spokes (λ s → distrib (r s) .snd) x i pair : n-Tr A (suc n) → n-Tr B (suc n) → n-Tr (A × B) (suc n) pair (inc x) (inc y) = inc (x , y) pair (inc x) (hub r) = hub λ s → pair (inc x) (r s) pair (inc x) (spokes r y i) = spokes (λ s → pair (inc x) (r s)) y i pair (hub r) y = hub λ s → pair (r s) y pair (spokes r x i) y = spokes (λ s → pair (r s) y) x i
open is-iso distrib-is-equiv : is-equiv distrib distrib-is-equiv = is-iso→is-equiv λ where .from (x , y) → pair x y .rinv → elim! λ x y → refl .linv → elim! λ x y → refl
For Σ
types, the
situation is slightly worse: the best we can do is show that
n-Tr-Σ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {n} → n-Tr (Σ A B) (suc n) ≃ n-Tr (Σ A λ a → n-Tr (B a) (suc n)) (suc n) n-Tr-Σ .fst = n-Tr-map (Σ-map id inc) n-Tr-Σ .snd = is-iso→is-equiv λ where .is-iso.from → rec! λ a b → inc (a , b) .is-iso.rinv → elim! λ a b → refl .is-iso.linv → elim! λ a b → refl
Moreover, we can show that if then the of a type is the same as directly
n-Tr-Tr : k ≤ n → n-Tr (n-Tr A (suc n)) (suc k) ≃ n-Tr A (suc k) n-Tr-Tr p .fst = let instance _ = p in rec! inc n-Tr-Tr p .snd = let instance _ = p in is-iso→is-equiv λ where .is-iso.from → n-Tr-rec! (n-Tr.inc ∘ n-Tr.inc) .is-iso.rinv → elim! λ x → refl .is-iso.linv → elim! λ x → refl
n-Tr∙ : ∀ (A∙ : Type∙ ℓ) n → Type∙ ℓ n-Tr∙ (A , a₀) n = n-Tr A n , inc a₀ inc∙ : ∀ {A∙ : Type∙ ℓ} {n} → A∙ →∙ n-Tr∙ A∙ n inc∙ = inc , refl n-Tr-prop : ∥ A ∥ ≃ n-Tr A 1 n-Tr-prop .fst = elim! n-Tr.inc n-Tr-prop .snd = is-iso→is-equiv (iso (elim! ∥_∥.inc) (elim! λ _ → refl) (elim! λ _ → refl)) n-Tr-set : ∥ A ∥₀ ≃ n-Tr A 2 n-Tr-set .fst = elim! n-Tr.inc n-Tr-set .snd = is-iso→is-equiv (iso (elim! ∥_∥₀.inc) (elim! λ _ → refl) (elim! λ _ → refl)) n-Tr-reindex : ∀ {ℓ} {A : Type ℓ} n k → n ≡ k → n-Tr A n ≃ n-Tr A k n-Tr-reindex zero zero p = id≃ n-Tr-reindex zero (suc k) p = absurd (zero≠suc p) n-Tr-reindex (suc n) zero p = absurd (suc≠zero p) n-Tr-reindex {A = A} (suc n) (suc k) p = done where instance _ : n ≤ k _ = ≤-refl' (suc-inj p) _ : k ≤ n _ = ≤-refl' (suc-inj (sym p)) done : n-Tr A (suc n) ≃ n-Tr A (suc k) done .fst = elim! inc done .snd = is-iso→is-equiv λ where .is-iso.from → elim! inc .is-iso.rinv → elim! λ x → refl .is-iso.linv → elim! λ x → refl n-Tr-reindex-inc : ∀ {ℓ} {A : Type ℓ} n k (p : n ≡ k) (x : A) → n-Tr-reindex n k p .fst (inc x) ≡ inc x n-Tr-reindex-inc zero zero p x = refl n-Tr-reindex-inc zero (suc k) p x = absurd (zero≠suc p) n-Tr-reindex-inc (suc n) zero p x = absurd (suc≠zero p) n-Tr-reindex-inc (suc n) (suc k) p x = refl n-Tr∙-reindex : ∀ {ℓ} {A : Type∙ ℓ} n k → n ≡ k → n-Tr∙ A n ≃∙ n-Tr∙ A k n-Tr∙-reindex n k p = n-Tr-reindex n k p , n-Tr-reindex-inc n k p _ n-Tr∙-reindex-inc : ∀ {ℓ} {A : Type∙ ℓ} n k (p : n ≡ k) → Equiv∙.to∙ (n-Tr∙-reindex n k p) ∘∙ inc∙ ≡ inc∙ {A∙ = A} n-Tr∙-reindex-inc n k p = funext∙ (n-Tr-reindex-inc n k p) (flip₁ (∙→square' (∙-idl _ ∙ sym (∙-idr _)))) instance n-Tr-homogeneous : ∀ {ℓ} {A : Type ℓ} {n} → ⦃ _ : Homogeneous A ⦄ → Homogeneous (n-Tr A (suc n)) n-Tr-homogeneous {A = A} {n} ⦃ h ⦄ {x} {y} = n-Tr-elim (λ x → ∀ y → (n-Tr A (suc n) , x) ≡ (n-Tr A (suc n) , y)) (λ x → Π-is-hlevel (suc n) λ _ → Type∙-path-is-hlevel n) (λ x → n-Tr-elim _ (λ _ → Type∙-path-is-hlevel n) (λ y → let e , pt = path→equiv∙ h in ua∙ (n-Tr-ap e , ap n-Tr.inc pt))) x y
Above, we established that truncations of paths are paths in truncations; this extends to a pointed equivalence between the of the loop space and the loop space of the of
n-Tr-Ω¹ : ∀ {ℓ} (A : Type∙ ℓ) n → n-Tr∙ (Ω¹ A) (1 + n) ≃∙ Ω¹ (n-Tr∙ A (2 + n)) n-Tr-Ω¹ A n = Equiv.inverse n-Tr-path-equiv , refl
n-Tr-Ω¹-inc : ∀ {ℓ} (A : Type∙ ℓ) n → Equiv∙.to∙ (n-Tr-Ω¹ A n) ∘∙ inc∙ ≡ Ω¹-map inc∙ n-Tr-Ω¹-inc A n = homogeneous-funext∙ (λ _ → sym (conj-refl _)) n-Tr-Ω¹-inv-inc : ∀ {ℓ} (A : Type∙ ℓ) n (l : ⌞ Ω¹ A ⌟) → Equiv.from (n-Tr-Ω¹ A n .fst) (Ω¹-map inc∙ .fst l) ≡ inc l n-Tr-Ω¹-inv-inc A n l = sym (Equiv.adjunctl (n-Tr-Ω¹ A n .fst) (n-Tr-Ω¹-inc A n ·ₚ l)) n-Tr-Ω¹-∙ : ∀ {ℓ} (A : Type∙ ℓ) n (p q : ⌞ Ω¹ A ⌟) → n-Tr-Ω¹ A n · inc (p ∙ q) ≡ (n-Tr-Ω¹ A n · inc p) ∙ (n-Tr-Ω¹ A n · inc q) n-Tr-Ω¹-∙ A n p q = ap-∙ inc p q
We can iterate this to show that the of the loop space is the loop space of the of
n-Tr-Ωⁿ : ∀ {ℓ} (A : Type∙ ℓ) n k → n-Tr∙ (Ωⁿ k A) (1 + n) ≃∙ Ωⁿ k (n-Tr∙ A (k + suc n)) n-Tr-Ωⁿ A n 0 = id≃ , refl n-Tr-Ωⁿ A n (suc k) = let fixup = Ωⁿ-ap (1 + k) (n-Tr∙-reindex (k + (2 + n)) (suc k + suc n) (+-sucr k (suc n))) in n-Tr∙ (Ωⁿ (1 + k) A) (suc n) ≃∙⟨⟩ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ≃∙⟨ n-Tr-Ω¹ (Ωⁿ k A) n ⟩≃∙ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ≃∙⟨ Ωⁿ-ap 1 (n-Tr-Ωⁿ A (suc n) k) ⟩≃∙ Ω¹ (Ωⁿ k (n-Tr∙ A (k + (2 + n)))) ≃∙⟨⟩ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ≃∙⟨ fixup ⟩≃∙ Ωⁿ (1 + k) (n-Tr∙ A (1 + k + suc n)) ≃∙∎
opaque unfolding Ω¹-ap -- The following lemmas demonstrate a useful proof technique: when showing -- an identity of the form (f ∘ g ∘ h) x ≡ y, we can proceed step -- by step by exhibiting a chain of *pointed* maps (in this case, -- pointed equivalences) from (X , x) to (Y , y) whose underlying -- function is f ∘ g ∘ h. -- This still involves some duplication, but at least it isn't -- quadratic in the number of functions. -- n-Tr-Ωⁿ respects path composition. n-Tr-Ωⁿ-∙ : ∀ {ℓ} (A : Type∙ ℓ) n k → (p q : ⌞ Ωⁿ (suc k) A ⌟) → n-Tr-Ωⁿ A n (suc k) · inc (p ∙ q) ≡ n-Tr-Ωⁿ A n (suc k) · inc p ∙ n-Tr-Ωⁿ A n (suc k) · inc q n-Tr-Ωⁿ-∙ A n k p q = trace .snd where trace : (n-Tr∙ (Ωⁿ (suc k) A) (1 + n) .fst , inc (p ∙ q)) ≃∙ (Ωⁿ (suc k) (n-Tr∙ A (suc k + suc n)) .fst , n-Tr-Ωⁿ A n (suc k) · inc p ∙ n-Tr-Ωⁿ A n (suc k) · inc q) trace = ⌞ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ⌟ , inc (p ∙ q) ≃∙⟨ n-Tr-Ω¹ _ n .fst , n-Tr-Ω¹-∙ _ _ p q ⟩≃∙ ⌞ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ⌟ , _ ≃∙⟨ Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) .fst , Ω¹-map-∙ (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) _ _ ⟩≃∙ ⌞ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ⌟ , _ ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ _) .fst , Ωⁿ-map-∙ k _ _ _ ⟩≃∙ ⌞ Ωⁿ (1 + k) (n-Tr∙ A (suc k + suc n)) ⌟ , _ ≃∙∎ -- n-Tr-Ωⁿ commutes with the obvious inclusions. n-Tr-Ωⁿ-inc : ∀ {ℓ} (A : Type∙ ℓ) n k → Equiv∙.to∙ (n-Tr-Ωⁿ A n k) ∘∙ inc∙ ≡ Ωⁿ-map k inc∙ n-Tr-Ωⁿ-inc A n zero = ∘∙-idl inc∙ n-Tr-Ωⁿ-inc A n (suc k) = homogeneous-funext∙ λ l → trace l .snd where trace : (l : ⌞ Ωⁿ (suc k) A ⌟) → (n-Tr∙ (Ωⁿ (suc k) A) (1 + n) .fst , inc l) ≃∙ (Ωⁿ (suc k) (n-Tr∙ A (suc k + suc n)) .fst , Ωⁿ-map (suc k) inc∙ .fst l) trace l = ⌞ n-Tr∙ (Ω¹ (Ωⁿ k A)) (suc n) ⌟ , inc l ≃∙⟨ n-Tr-Ω¹ _ n .fst , n-Tr-Ω¹-inc _ n ·ₚ l ⟩≃∙ ⌞ Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) ⌟ , l¹ ≃∙⟨ Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) .fst , pt1 ⟩≃∙ ⌞ Ωⁿ (1 + k) (n-Tr∙ A (k + (2 + n))) ⌟ , lᵏ ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ _) .fst , pt2 ⟩≃∙ ⌞ Ωⁿ (1 + k) (n-Tr∙ A (1 + k + suc n)) ⌟ , lᵏ ≃∙∎ where l¹ : Ω¹ (n-Tr∙ (Ωⁿ k A) (2 + n)) .fst l¹ = Ω¹-map inc∙ .fst l lᵏ : ∀ {n} → ⌞ Ωⁿ (suc k) (n-Tr∙ A n) ⌟ lᵏ = Ωⁿ-map (1 + k) inc∙ .fst l pt1 : Ω¹-ap (n-Tr-Ωⁿ A (suc n) k) · l¹ ≡ lᵏ pt1 = Ω¹-map (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) .fst l¹ ≡⟨ Ω¹-map-∘ (Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k)) inc∙ ·ₚ l ⟩≡ Ω¹-map ⌜ Equiv∙.to∙ (n-Tr-Ωⁿ A (suc n) k) ∘∙ inc∙ ⌝ .fst l ≡⟨ ap! (n-Tr-Ωⁿ-inc A (suc n) k) ⟩≡ Ω¹-map (Ωⁿ-map k inc∙) .fst l ∎ pt2 : Ωⁿ-ap (1 + k) (n-Tr∙-reindex _ _ (+-sucr k (suc n))) · lᵏ ≡ lᵏ pt2 = (Ωⁿ-map-∘ (1 + k) _ inc∙ ·ₚ l) ∙ ap (λ x → Ωⁿ-map (1 + k) x .fst l) (n-Tr∙-reindex-inc (k + (2 + n)) _ _)
Any map can be made basepoint-preserving by letting be based at ↩︎