Homotopy Type Theory Whitehead's principle > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


< Whitehead's principle

Whitehead’s principle says that given types

AA and BB and function f:ABf:A \to B, if the set-truncation of ff is an equivalence and the nn-th homotopy group of ff is an equivalence, then ff is an equivalence.

AtypeBtypef:ABp:isEquiv([f] 0)q: n:isEquiv(π n(f))r:isEquiv(f)\frac{A\ \mathrm{type} \quad B\ \mathrm{type} \quad f:A \to B \quad p:\mathrm{isEquiv}(\left[f\right]_0) \quad q:\prod_{n:\mathbb{N}} \mathrm{isEquiv}(\pi^n(f))}{r:\mathrm{isEquiv}(f)}

In universes

Whitehead’s principle is said to hold in a universe 𝒰\mathcal{U} if the universe comes with a dependent function

p: A:𝒰 B:𝒰 f:𝒯 𝒰(A)𝒯 𝒰(B)(isEquiv([f] 0)× n:isEquiv(π n(f)))isEquiv(f)p:\prod_{A:\mathcal{U}} \prod_{B:\mathcal{U}} \prod_{f:\mathcal{T}_\mathcal{U}(A) \to \mathcal{T}_\mathcal{U}(B)} \left(\mathrm{isEquiv}(\left[f\right]_0) \times \prod_{n:\mathbb{N}} \mathrm{isEquiv}(\pi^n(f))\right) \to \mathrm{isEquiv}(f)

See also

Last revised on June 14, 2022 at 04:43:28. See the history of this page for a list of all contributions to it.