Contractible maps

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-07.
Last modified on 2024-02-19.

module foundation-core.contractible-maps where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.coherently-invertible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


A map is often said to satisfy a property P if each of its fibers satisfy property P. Thus, we define contractible maps to be maps of which each fiber is contractible. In other words, contractible maps are maps f : A → B such that for each element b : B there is a unique a : A equipped with an identification (f a) = b, i.e., contractible maps are the type theoretic bijections.


module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  is-contr-map : (A  B)  UU (l1  l2)
  is-contr-map f = (y : B)  is-contr (fiber f y)


Any contractible map is an equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}

  map-inv-is-contr-map : is-contr-map f  B  A
  map-inv-is-contr-map H y = pr1 (center (H y))

  is-section-map-inv-is-contr-map :
    (H : is-contr-map f)  (f  (map-inv-is-contr-map H)) ~ id
  is-section-map-inv-is-contr-map H y = pr2 (center (H y))

  is-retraction-map-inv-is-contr-map :
    (H : is-contr-map f)  ((map-inv-is-contr-map H)  f) ~ id
  is-retraction-map-inv-is-contr-map H x =
      ( pr1 {B = λ z  (f z)  (f x)})
      ( ( inv
          ( contraction
            ( H (f x))
            ( ( map-inv-is-contr-map H (f x)) ,
              ( is-section-map-inv-is-contr-map H (f x))))) 
        ( contraction (H (f x)) (x , refl)))

    is-equiv-is-contr-map : is-contr-map f  is-equiv f
    is-equiv-is-contr-map H =
        ( map-inv-is-contr-map H)
        ( is-section-map-inv-is-contr-map H)
        ( is-retraction-map-inv-is-contr-map H)

Any coherently invertible map is a contractible map

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}

    center-fiber-is-coherently-invertible :
      is-coherently-invertible f  (y : B)  fiber f y
    pr1 (center-fiber-is-coherently-invertible H y) =
      map-inv-is-coherently-invertible H y
    pr2 (center-fiber-is-coherently-invertible H y) =
      is-section-map-inv-is-coherently-invertible H y

    contraction-fiber-is-coherently-invertible :
      (H : is-coherently-invertible f)  (y : B)  (t : fiber f y) 
      (center-fiber-is-coherently-invertible H y)  t
    contraction-fiber-is-coherently-invertible H y (x , refl) =
      eq-Eq-fiber f y
        ( is-retraction-map-inv-is-coherently-invertible H x)
        ( ( right-unit) 
          ( inv ( coh-is-coherently-invertible H x)))

  is-contr-map-is-coherently-invertible :
    is-coherently-invertible f  is-contr-map f
  pr1 (is-contr-map-is-coherently-invertible H y) =
    center-fiber-is-coherently-invertible H y
  pr2 (is-contr-map-is-coherently-invertible H y) =
    contraction-fiber-is-coherently-invertible H y

Any equivalence is a contractible map

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}

    is-contr-map-is-equiv : is-equiv f  is-contr-map f
    is-contr-map-is-equiv =
      is-contr-map-is-coherently-invertible  is-coherently-invertible-is-equiv

See also

Recent changes