From 43094ddf1274256e21ab95adbaac27871e0ef651 Mon Sep 17 00:00:00 2001 From: Alice Laroche Date: Thu, 1 Oct 2026 17:44:05 +0200 Subject: [PATCH 1/4] defn: Whitehead's theorem --- src/1Lab/Equiv.lagda.md | 8 +++ src/Homotopy/Loopspace.lagda.md | 15 +++++ src/Homotopy/Whitehead.lagda.md | 116 ++++++++++++++++++++++++++++++++ 3 files changed, 139 insertions(+) create mode 100644 src/Homotopy/Whitehead.lagda.md diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md index b7b4b5dd7..488c05832 100644 --- a/src/1Lab/Equiv.lagda.md +++ b/src/1Lab/Equiv.lagda.md @@ -1232,6 +1232,14 @@ is-equiv≃fibre-is-contr {f = f} = is-eqv (λ fib-contr → record { is-eqv = fib-contr }) +is-equiv-if-inhabited→is-equiv + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} + → (f : A → B) + → (B → is-equiv f) + → is-equiv f +is-equiv-if-inhabited→is-equiv f h = E.from λ x → E.to (h x) x + where open module E = Equiv is-equiv≃fibre-is-contr + -- This ideally would go in 1Lab.HLevel, but we don't have equivalences -- defined that early in the bootrapping process. is-prop→is-contr-iff-inhabited diff --git a/src/Homotopy/Loopspace.lagda.md b/src/Homotopy/Loopspace.lagda.md index 02f48f54f..edf2627de 100644 --- a/src/Homotopy/Loopspace.lagda.md +++ b/src/Homotopy/Loopspace.lagda.md @@ -80,6 +80,21 @@ zero map. + +```agda +module Homotopy.Whitehead where +``` + +# Whitehead's theorem + +In classical homotopy theory, **Whitehead's theorem** states that if a functions +$f : A \to B$ induces isomorphisms between $\pi_n(A, a)$ and $\pi_n(B, f(a))$ +for all points $a$ in $A$, it is itself an equivalence. + +```agda +∥-∥₀-is-surjective→is-surjective + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) + → is-surjective (∥-∥₀-map f) + → is-surjective f +∥-∥₀-is-surjective→is-surjective {A = A} f ∥-∥-is-surj b = + ∥-∥-rec squash rec₂ $ ∥-∥-is-surj (inc b) + where + P : ∥ A ∥₀ → Type _ + P a = ∥-∥₀-map f a ≡ inc b → ∥ fibre f b ∥ + + rec₁ : ∀ a → P (inc a) + rec₁ a p = ∥-∥-rec squash (λ p → inc (a , p)) (∥-∥₀-path-equiv .fst p) + + rec₂ : fibre (∥-∥₀-map f) (inc b) → ∥ fibre f b ∥ + rec₂ (a , p) = ∥-∥₀-elim (λ a → hlevel {T = P a} 2) rec₁ a p + +embeding-∥-∥₀-surjective→is-equiv + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) + → is-surjective (∥-∥₀-map f) + → is-embedding f + → is-equiv f +embeding-∥-∥₀-surjective→is-equiv f is-surj is-embed = + embedding-surjective→is-equiv is-embed $ + (∥-∥₀-is-surjective→is-surjective f is-surj) + +Ω¹-map-is-equiv→is-cancellable + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) + → is-equiv (∥-∥₀-map f) + → (∀ x → is-equiv (Ω¹-map {A = (A , x)} (f , refl) .fst)) + → {x y : A} → (x ≡ y) ≃ (f x ≡ f y) +Ω¹-map-is-equiv→is-cancellable f is-eqv Ω¹-is-equiv {x} {y} = + (ap f) , is-equiv-if-inhabited→is-equiv (ap f) isequiv + where + x≡y : f x ≡ f y → ∥ x ≡ y ∥ + x≡y p = ∥-∥₀-path-equiv .fst $ equiv→inverse (equiv→cancellable is-eqv) (ap inc p) + + ap-is-equiv : (p : x ≡ y) → is-equiv {A = x ≡ y} (ap f) + ap-is-equiv = J (λ y _ → is-equiv {A = x ≡ y} (ap f)) + (subst is-equiv (λ i → Ω¹-map-refl {A = _ , x} f i .fst) (Ω¹-is-equiv x)) + + isequiv : f x ≡ f y → is-equiv (ap f) + isequiv p = ∥-∥-rec (is-equiv-is-prop _) ap-is-equiv (x≡y p) + +Ω¹-map-is-equiv→is-equiv + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) + → is-equiv (∥-∥₀-map f) + → (∀ x → is-equiv (Ω¹-map {A = A , x} (f , refl) .fst)) + → is-equiv f +Ω¹-map-is-equiv→is-equiv {A = A} {B} f is-eqv Ω¹-is-equiv = + embeding-∥-∥₀-surjective→is-equiv f + (is-equiv→is-surjective is-eqv) + (cancellable→embedding (Ω¹-map-is-equiv→is-cancellable f is-eqv Ω¹-is-equiv e⁻¹)) + +π-sucP : ∀ {ℓ} n (A : Type∙ ℓ) → ⌞ πₙ₊₁ (suc n) A ⌟ ≡ ⌞ πₙ₊₁ n (Ω¹ A) ⌟ +π-sucP n A i = ∥ Ω¹ (Ωⁿ-sucP A n i) .fst ∥₀ + +π-suc-naturalP : ∀ {ℓ} n {A : Type∙ ℓ} {B : Type∙ ℓ} (f : A →∙ B) + → PathP (λ i → π-sucP n A i → π-sucP n B i) + (πₙ₊₁-map (suc n) f) (πₙ₊₁-map n (Ω¹-map f)) +π-suc-naturalP n f i = ∥-∥₀-map (Ω¹-map (Ω-suc-naturalP n f i) .fst) + +π-map-is-equiv→is-equiv + : ∀ {ℓ} n {A : Type ℓ} {B : Type ℓ} + → is-hlevel A n → is-hlevel B n + → (f : A → B) + → is-equiv (∥-∥₀-map f) + → (∀ x k → is-equiv (πₙ₊₁-map {A = A , x} k (f , refl))) + → is-equiv f +π-map-is-equiv→is-equiv zero A-hlvl B-hlvl f is-eqv π-is-equiv = + is-contr→is-equiv A-hlvl B-hlvl +π-map-is-equiv→is-equiv (suc n) A-hlvl B-hlvl f is-eqv π-is-equiv = isequiv + where + π-ap-is-equiv : ∀ x y k (p : x ≡ y) → is-equiv (πₙ₊₁-map {A = _ , p} k (ap f , refl)) + π-ap-is-equiv x y k = + J (λ _ p → is-equiv (πₙ₊₁-map {A = _ , p} k (ap f , refl))) + (substd is-equiv (π-suc-naturalP k (f , refl) ▷ ap (πₙ₊₁-map k) (Ω¹-map-refl f)) + (π-is-equiv x (suc k))) + + isequiv : is-equiv f + isequiv = Ω¹-map-is-equiv→is-equiv f is-eqv λ x → π-map-is-equiv→is-equiv n + (Path-is-hlevel' _ A-hlvl x x) + (Path-is-hlevel' _ B-hlvl (f x) (f x)) + (Ω¹-map (f , refl) .fst) + (π-is-equiv x 0) + (λ p k → substd (λ f → is-equiv (πₙ₊₁-map k f)) + (symP (Ω¹-map-refl' f p)) + (π-ap-is-equiv x x k p)) + ``` From 39c8eb490993313dd106b64421f39ca4f62e19e7 Mon Sep 17 00:00:00 2001 From: Alice Laroche Date: Thu, 1 Oct 2026 17:46:32 +0200 Subject: [PATCH 2/4] fixup: sorting import --- src/Homotopy/Whitehead.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Homotopy/Whitehead.lagda.md b/src/Homotopy/Whitehead.lagda.md index 4e1003175..ef1e9b10c 100644 --- a/src/Homotopy/Whitehead.lagda.md +++ b/src/Homotopy/Whitehead.lagda.md @@ -7,11 +7,11 @@ open import Algebra.Group.Cat.Base open import Algebra.Group.Homotopy open import Algebra.Group +open import Data.Set.Truncation + open import Homotopy.Space.Delooping open import Homotopy.Conjugation open import Homotopy.Loopspace - -open import Data.Set.Truncation ``` --> From 07bebc2a90a4d32e6d7ab55cabd6b39dbbd5dbee Mon Sep 17 00:00:00 2001 From: Alice Laroche <60161310+alicelaroche@users.noreply.github.com> Date: Thu, 1 Oct 2026 18:43:15 +0200 Subject: [PATCH 3/4] Apply batched suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Amélia Liao --- src/Homotopy/Whitehead.lagda.md | 74 ++++++++++++++++----------------- 1 file changed, 37 insertions(+), 37 deletions(-) diff --git a/src/Homotopy/Whitehead.lagda.md b/src/Homotopy/Whitehead.lagda.md index ef1e9b10c..d5d39e529 100644 --- a/src/Homotopy/Whitehead.lagda.md +++ b/src/Homotopy/Whitehead.lagda.md @@ -31,16 +31,15 @@ for all points $a$ in $A$, it is itself an equivalence. → is-surjective (∥-∥₀-map f) → is-surjective f ∥-∥₀-is-surjective→is-surjective {A = A} f ∥-∥-is-surj b = - ∥-∥-rec squash rec₂ $ ∥-∥-is-surj (inc b) - where - P : ∥ A ∥₀ → Type _ - P a = ∥-∥₀-map f a ≡ inc b → ∥ fibre f b ∥ + ∥-∥-rec squash rec₂ $ ∥-∥-is-surj (inc b) where + P : ∥ A ∥₀ → Type _ + P a = ∥-∥₀-map f a ≡ inc b → ∥ fibre f b ∥ - rec₁ : ∀ a → P (inc a) - rec₁ a p = ∥-∥-rec squash (λ p → inc (a , p)) (∥-∥₀-path-equiv .fst p) + rec₁ : ∀ a → P (inc a) + rec₁ a p = ∥-∥-rec squash (λ p → inc (a , p)) (∥-∥₀-path-equiv .fst p) - rec₂ : fibre (∥-∥₀-map f) (inc b) → ∥ fibre f b ∥ - rec₂ (a , p) = ∥-∥₀-elim (λ a → hlevel {T = P a} 2) rec₁ a p + rec₂ : fibre (∥-∥₀-map f) (inc b) → ∥ fibre f b ∥ + rec₂ (a , p) = ∥-∥₀-elim (λ a → hlevel {T = P a} 2) rec₁ a p embeding-∥-∥₀-surjective→is-equiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) @@ -57,17 +56,16 @@ embeding-∥-∥₀-surjective→is-equiv f is-surj is-embed = → (∀ x → is-equiv (Ω¹-map {A = (A , x)} (f , refl) .fst)) → {x y : A} → (x ≡ y) ≃ (f x ≡ f y) Ω¹-map-is-equiv→is-cancellable f is-eqv Ω¹-is-equiv {x} {y} = - (ap f) , is-equiv-if-inhabited→is-equiv (ap f) isequiv - where - x≡y : f x ≡ f y → ∥ x ≡ y ∥ - x≡y p = ∥-∥₀-path-equiv .fst $ equiv→inverse (equiv→cancellable is-eqv) (ap inc p) + ap f , is-equiv-if-inhabited→is-equiv (ap f) isequiv where + x≡y : f x ≡ f y → ∥ x ≡ y ∥ + x≡y p = ∥-∥₀-path-equiv .fst $ equiv→inverse (equiv→cancellable is-eqv) (ap inc p) - ap-is-equiv : (p : x ≡ y) → is-equiv {A = x ≡ y} (ap f) - ap-is-equiv = J (λ y _ → is-equiv {A = x ≡ y} (ap f)) - (subst is-equiv (λ i → Ω¹-map-refl {A = _ , x} f i .fst) (Ω¹-is-equiv x)) + ap-is-equiv : (p : x ≡ y) → is-equiv {A = x ≡ y} (ap f) + ap-is-equiv = J (λ y _ → is-equiv {A = x ≡ y} (ap f)) + (subst is-equiv (λ i → Ω¹-map-refl {A = _ , x} f i .fst) (Ω¹-is-equiv x)) - isequiv : f x ≡ f y → is-equiv (ap f) - isequiv p = ∥-∥-rec (is-equiv-is-prop _) ap-is-equiv (x≡y p) + isequiv : f x ≡ f y → is-equiv (ap f) + isequiv p = ∥-∥-rec (is-equiv-is-prop _) ap-is-equiv (x≡y p) Ω¹-map-is-equiv→is-equiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) @@ -82,9 +80,10 @@ embeding-∥-∥₀-surjective→is-equiv f is-surj is-embed = π-sucP : ∀ {ℓ} n (A : Type∙ ℓ) → ⌞ πₙ₊₁ (suc n) A ⌟ ≡ ⌞ πₙ₊₁ n (Ω¹ A) ⌟ π-sucP n A i = ∥ Ω¹ (Ωⁿ-sucP A n i) .fst ∥₀ -π-suc-naturalP : ∀ {ℓ} n {A : Type∙ ℓ} {B : Type∙ ℓ} (f : A →∙ B) - → PathP (λ i → π-sucP n A i → π-sucP n B i) - (πₙ₊₁-map (suc n) f) (πₙ₊₁-map n (Ω¹-map f)) +π-suc-naturalP + : ∀ {ℓ} n {A : Type∙ ℓ} {B : Type∙ ℓ} (f : A →∙ B) + → PathP (λ i → π-sucP n A i → π-sucP n B i) + (πₙ₊₁-map (suc n) f) (πₙ₊₁-map n (Ω¹-map f)) π-suc-naturalP n f i = ∥-∥₀-map (Ω¹-map (Ω-suc-naturalP n f i) .fst) π-map-is-equiv→is-equiv @@ -96,21 +95,22 @@ embeding-∥-∥₀-surjective→is-equiv f is-surj is-embed = → is-equiv f π-map-is-equiv→is-equiv zero A-hlvl B-hlvl f is-eqv π-is-equiv = is-contr→is-equiv A-hlvl B-hlvl -π-map-is-equiv→is-equiv (suc n) A-hlvl B-hlvl f is-eqv π-is-equiv = isequiv - where - π-ap-is-equiv : ∀ x y k (p : x ≡ y) → is-equiv (πₙ₊₁-map {A = _ , p} k (ap f , refl)) - π-ap-is-equiv x y k = - J (λ _ p → is-equiv (πₙ₊₁-map {A = _ , p} k (ap f , refl))) - (substd is-equiv (π-suc-naturalP k (f , refl) ▷ ap (πₙ₊₁-map k) (Ω¹-map-refl f)) - (π-is-equiv x (suc k))) - - isequiv : is-equiv f - isequiv = Ω¹-map-is-equiv→is-equiv f is-eqv λ x → π-map-is-equiv→is-equiv n - (Path-is-hlevel' _ A-hlvl x x) - (Path-is-hlevel' _ B-hlvl (f x) (f x)) - (Ω¹-map (f , refl) .fst) - (π-is-equiv x 0) - (λ p k → substd (λ f → is-equiv (πₙ₊₁-map k f)) - (symP (Ω¹-map-refl' f p)) - (π-ap-is-equiv x x k p)) +π-map-is-equiv→is-equiv (suc n) A-hlvl B-hlvl f is-eqv π-is-equiv = isequiv where + π-ap-is-equiv + : ∀ x y k (p : x ≡ y) + → is-equiv (πₙ₊₁-map {A = _ , p} k (ap f , refl)) + π-ap-is-equiv x y k = + J (λ _ p → is-equiv (πₙ₊₁-map {A = _ , p} k (ap f , refl))) + (substd is-equiv (π-suc-naturalP k (f , refl) ▷ ap (πₙ₊₁-map k) (Ω¹-map-refl f)) + (π-is-equiv x (suc k))) + + isequiv : is-equiv f + isequiv = Ω¹-map-is-equiv→is-equiv f is-eqv λ x → π-map-is-equiv→is-equiv n + (Path-is-hlevel' _ A-hlvl x x) + (Path-is-hlevel' _ B-hlvl (f x) (f x)) + (Ω¹-map (f , refl) .fst) + (π-is-equiv x 0) + (λ p k → substd (λ f → is-equiv (πₙ₊₁-map k f)) + (symP (Ω¹-map-refl' f p)) + (π-ap-is-equiv x x k p)) ``` From a87b3573b0b3ff731b5bb6b1a9dd24a81c3c8dc8 Mon Sep 17 00:00:00 2001 From: Alice Laroche Date: Mon, 5 Oct 2026 22:44:19 +0200 Subject: [PATCH 4/4] fixup: moved some definitions + proof tweaking --- src/Algebra/Group/Homotopy.lagda.md | 8 ++++ src/Data/Set/Truncation.lagda.md | 56 ++++++++++++++++++++++ src/Homotopy/Whitehead.lagda.md | 73 ++++++++++------------------- 3 files changed, 88 insertions(+), 49 deletions(-) diff --git a/src/Algebra/Group/Homotopy.lagda.md b/src/Algebra/Group/Homotopy.lagda.md index d5ba0d3af..919cc74cd 100644 --- a/src/Algebra/Group/Homotopy.lagda.md +++ b/src/Algebra/Group/Homotopy.lagda.md @@ -89,6 +89,14 @@ opaque : ∀ {ℓ} (A : Type∙ ℓ) n p q → πₙ-def A n · inc (p ∙ q) ≡ πₙ-def A n · inc p ∙ πₙ-def A n · inc q πₙ-def-∙ A = n-Tr-Ωⁿ-∙ A 1 + +π-sucP : ∀ {ℓ} n (A : Type∙ ℓ) → ⌞ πₙ₊₁ (suc n) A ⌟ ≡ ⌞ πₙ₊₁ n (Ω¹ A) ⌟ +π-sucP n A i = ∥ Ω¹ (Ωⁿ-sucP A n i) .fst ∥₀ + +π-suc-naturalP : ∀ {ℓ} n {A : Type∙ ℓ} {B : Type∙ ℓ} (f : A →∙ B) + → PathP (λ i → π-sucP n A i → π-sucP n B i) + (πₙ₊₁-map (suc n) f) (πₙ₊₁-map n (Ω¹-map f)) +π-suc-naturalP n f i = ∥-∥₀-map (Ω¹-map (Ω-suc-naturalP n f i) .fst) ``` --> diff --git a/src/Data/Set/Truncation.lagda.md b/src/Data/Set/Truncation.lagda.md index 0be127376..66636f2b1 100644 --- a/src/Data/Set/Truncation.lagda.md +++ b/src/Data/Set/Truncation.lagda.md @@ -1,6 +1,8 @@