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

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