The Whitehead principle for maps

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-maps where
Imports 
open import foundation.connected-maps
open import foundation.connected-types
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.infinity-connected-maps
open import foundation.infinity-connected-types
open import foundation.truncation-levels
open import foundation.truncations
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.propositions

open import synthetic-homotopy-theory.whitehead-principle-types

Idea

The Whitehead principle for maps asserts that ∞-connected maps are equivalences. I.e., if the fibers of a map f : X → Y are ∞-connected, then it is an equivalence. This principle is also referred to as hypercompleteness and is not validated in every ∞-topos.

Definition

Whitehead-Principle-Map-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Whitehead-Principle-Map-Level l1 l2 =
  ( X : UU l1) → (Y : UU l2) → (f : X → Y) → is-∞-connected-map f → is-equiv f

Whitehead-Principle-Map : UUω
Whitehead-Principle-Map = {l1 l2 : Level} → Whitehead-Principle-Map-Level l1 l2

Properties

The Whitehead principle for maps implies the Whitehead principle for types

Whitehead-Principle-Maps-implies-Types :
  Whitehead-Principle-Map → Whitehead-Principle
Whitehead-Principle-Maps-implies-Types WP X is-∞-conn-X =
  is-contr-equiv-unit eq
  where
    eq : X ≃ unit
    pr1 eq = terminal-map X
    pr2 eq =
      WP X unit (terminal-map X)
        ( λ x → is-∞-connected-equiv
          ( equiv-fiber-terminal-map star) is-∞-conn-X)

The Whitehead principle for types implies the Whitehead principle for maps

Whitehead-Principle-Types-implies-Maps :
  Whitehead-Principle → Whitehead-Principle-Map
Whitehead-Principle-Types-implies-Maps WP X Y f is-∞-conn-f =
  is-equiv-is-contr-map is-contr-map-f
  where
    is-contr-map-f : is-contr-map f
    is-contr-map-f y = WP (fiber f y) (λ x → is-∞-conn-f y x)

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