The Whitehead principle for types
Content created by Fredrik Bakke and Garrett Figueroa.
Created on 2025-07-27.
Last modified on 2025-07-27.
module synthetic-homotopy-theory.whitehead-principle-types where
Imports
open import foundation.connected-types open import foundation.dependent-pair-types open import foundation.functoriality-truncation open import foundation.infinity-connected-types open import foundation.truncation-levels open import foundation.truncations open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.identity-types open import foundation-core.propositions
Idea
The Whitehead principle¶ asserts that ∞-connected types are contractible. I.e., if a type is -connected for every , then it is contractible. This principle is also referred to as hypercompleteness and is not validated in every ∞-topos.
In
(whitehead-principle-maps
)[synthetic-homotopy-theory.whitehead-principle-maps.md]
we show, assuming the Whitehead principle in enough universes, that the
Whitehead principle for types is
equivalent to asking that maps whose
fibers are ∞-connected are
equivalences.
Definition
Whitehead-Principle-Level : (l : Level) → UU (lsuc l) Whitehead-Principle-Level l = (X : UU l) → is-∞-connected X → is-contr X Whitehead-Principle : UUω Whitehead-Principle = {l : Level} → Whitehead-Principle-Level l
See also
External links
- hypercomplete object on Lab
- Whitehead theorem on Wikipedia
References
For the equivalent concept in the ∞-categorical semantics of homotopy type theory, cf. §6.5.2 of Lurie’s Higher Topos Theory [Lur09].
- [Lur09]
- Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009. ISBN 9780691140490. URL: https://www.math.ias.edu/~lurie/papers/highertopoi.pdf.
Recent changes
- 2025-07-27. Garrett Figueroa and Fredrik Bakke. The Whitehead principle (#1453).