open import 1Lab.Path.Reasoning
open import 1Lab.Prelude

open import Data.Nat.Properties
open import Data.Set.Truncation
open import Data.Nat.Order
open import Data.Nat.Base
open import Data.List using (_∷_ ; [])

open import Homotopy.Space.Suspension
open import Homotopy.Space.Sphere
open import Homotopy.Conjugation
open import Homotopy.Loopspace

module Homotopy.Truncation where

private variable
  ℓ ℓ'  : Level
  A B C : Type ℓ
  n k   : Nat

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 $f : S^{n} \to A$ is equivalently some loop in $A$ ¹, we can characterise the trivial loops as the constant functions $S^{n} \to A .$ Correspondingly, if every function $S^{n} \to A$ is trivial, this means that all $n -loops$ in $A$ are trivial, so that $A$ is $(n + 1) -truncated!$

We refer to a trivialisation of a map $f : S^{n} \to A$ as being a “hubs-and-spokes” construction. Geometrically, a trivial loop $f : S^{n} \to A$ can be understood as a map from the $n -$ disc rather than the $n -sphere,$ where the $n -disc$ 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 $n -truncation$ 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 $n -truncated,$ what we can do is freely generate hubs and spokes for any $n -sphere$ drawn on the $n -truncation$ of $A .$ The result is the universal $n -type$ admitting a map from $A .$

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 $n -truncation$ has the right h-level, and proving that one can eliminate from it to $n -types,$ 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 $n -truncation$ of $A$ is characterising its path spaces, at least for the inclusions of points from $A .$ Identifications between (the images of) points in $A$ in the $(n + 1) -truncation$ are equivalently $n -truncated$ identifications in $A :$

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

inc (x) \equiv_{∥ A ∥_{2 + n}} y,

so we will, for every $x : A,$ define a type family $code (x) : ∥ A ∥_{2 + n} \to Type,$ where the fibre of $code (x)$ over $inc (y)$ should be $∥ x \equiv y ∥_{1 + n} .$ However, the induction principle for $∥ A ∥_{2 + n}$ only allows us to map into $(2 + n) -types,$ while $Type$ itself is not an $n -type$ for any $n .$ We salvage our definition by instead mapping into $(1 + n) - Type,$ which is a $(2 + n) -type.$

  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 $∥ A ∥_{n + 2} .$

  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 $∥ A ∥_{n}$ and functions out of $A,$ 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 $n -truncation$ 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 $∥ ∥ x : A \sum B (x) ∥ ∥_{n} ≃ ∥ ∥ x : A \sum ∥ B (x) ∥_{n} ∥ ∥_{n} .$

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 $k \leq n,$ then $k -truncating$ the $n -truncation$ of a type $A$ is the same as directly $k -truncating$ $A .$

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 $n -truncation$ of the loop space $Ω A$ and the loop space of the $(1 + n) -truncation$ of $A .$

opaque
  unfolding Ω¹-map

  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 $n -truncation$ of the $k -fold$ loop space $∥ Ω^{k} A ∥_{n}$ is the $k -fold$ loop space of the $(k + n) -truncation$ of $A .$

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 $f : S^{n} \to A$ can be made basepoint-preserving by letting $A$ be based at $f (N) .$ ↩︎