defn: Whitehead's theorem

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

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)
 ```
 -->
 

src/Data/Set/Truncation.lagda.md

@@ -1,6 +1,8 @@
 <!--
 ```agda
+open import 1Lab.Function.Surjection
 open import 1Lab.Path.IdentitySystem
+open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Universe
 open import 1Lab.HLevel.Closure
@@ -145,8 +147,62 @@ module ∥-∥₀-path {ℓ} {A : Type ℓ} {x} {y}
   = Equiv (∥-∥₀-path-equiv {A = A} {x} {y})
 ```
 
+# Surjectivity and set truncation
+
+It can be shown that a function $f$ is [[surjective | surjection ]] when it is surjective
+at the level of set truncations.
+
+Indeed, `f` being surjective at the level of sets means that there merely exists an
+$a : \| A \|_0$ such that $\| f b \|_0 = a$. Because what we want to prove is a mere
+proposition and thus also a set, we can assume an $a : A$ such that it is merely equal to $f b$.
+
+Because what we want to prove is still a mere proposition, we can then assume $f b = a$
+and give an inhabitant of $fibre f b$.
+
+The converse can be proven in a similar fashion.
+```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)) (Equiv.to ∥-∥₀-path-equiv p)
+
+  rec₂ : fibre (∥-∥₀-map f) (inc b) → ∥ fibre f b ∥
+  rec₂ (a , p) = ∥-∥₀-elim (λ a → hlevel {T = P a} 2) rec₁ a p
+
+is-surjective→∥-∥₀-is-surjective
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B)
+  → is-surjective f
+  → is-surjective (∥-∥₀-map f)
+is-surjective→∥-∥₀-is-surjective {B = B} f is-surj b =
+  ∥-∥₀-elim (λ b → hlevel {T = P b} 2) (λ b → ∥-∥-map (rec b) (is-surj b)) b
+  where
+  P : ∥ B ∥₀ → Type _
+  P b = ∥ fibre (∥-∥₀-map f) b ∥
+
+  rec : ∀ b → fibre f b → fibre (∥-∥₀-map f) (inc b)
+  rec b (a , p) = inc a , ap inc p
+
+```
 <!--
 ```agda
+
+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)
+
 instance
   H-Level-∥-∥₀ : ∀ {ℓ} {A : Type ℓ} {n : Nat} → H-Level ∥ A ∥₀ (2 + n)
   H-Level-∥-∥₀ {n = n} = basic-instance 2 squash

src/Homotopy/Loopspace.lagda.md

@@ -80,6 +80,21 @@ zero map.
 
 <!--
 ```agda
+  Ω¹-map-refl
+    : ∀ {ℓ'} {B : Type ℓ'} (f : A .fst → B)
+    → Path (Ω¹ A →∙ Ω¹ (B , f (A .snd))) (Ω¹-map (f , refl)) (ap f , refl)
+  Ω¹-map-refl f i .fst α = conj-refl (ap f α) i
+  Ω¹-map-refl f i .snd = conj-refl-square i
+
+  Ω¹-map-refl'
+    : ∀ {ℓ'} {B : Type ℓ'} (f : A .fst → B)
+    → (p : A .snd ≡ A .snd)
+    → PathP (λ i → A .snd ≡ A .snd , p →∙ f (A .snd) ≡ f (A .snd) , Ω¹-map-refl f i .fst p)
+       (Ω¹-map {A = A} (f , refl) .fst , refl)
+       (ap f , refl)
+  Ω¹-map-refl' f p i .fst α = conj-refl (ap f α) i
+  Ω¹-map-refl' f p i .snd = refl
+
 Ω¹-map∙ : Maps∙ A B →∙ Maps∙ (Ω¹ A) (Ω¹ B)
 Ω¹-map∙ .fst = Ω¹-map
 Ω¹-map∙ .snd = Ω¹-map-zero

src/Homotopy/Whitehead.lagda.md

@@ -0,0 +1,91 @@
+<!--
+```agda
+open import 1Lab.Path.Reasoning
+open import 1Lab.Prelude
+
+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
+```
+-->
+
+```agda
+module Homotopy.Whitehead where
+```
+
+# Whitehead's theorem
+
+In classical homotopy theory, **Whitehead's theorem** states that if a function
+$f : A \to B$ induces [[isomorphisms|quasi-inverse]] between $\pi_n(A, a)$ and $\pi_n(B, f(a))$
+for all points $a$ in $A$, it is itself an [[equivalence]].
+
+In homotopy type theory however, this statement doesn't not hold in general.
+Instead we can prove it for any [[n-types]] by induction on n by first constructing
+an equivalence between the trivial higher loopspace and working downward from there.
+
+```agda
+Ω¹-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-on-loop : is-equiv {A = x ≡ x} (ap f)
+    ap-is-equiv-on-loop =
+      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)) ap-is-equiv-on-loop
+
+    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⁻¹))
+
+π-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} 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)))
+
+  step : (x : A) → is-equiv (Ω¹-map (f , refl) .fst)
+  step 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))
+
+  isequiv : is-equiv f
+  isequiv = Ω¹-map-is-equiv→is-equiv f is-eqv step
+```