Contractible maps

module foundation-core.contractible-maps where

Imports

open import foundation-core.coherently-invertible-maps
open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.universe-levels

Idea

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.

Definition

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

  is-contr-map : (A → B) → UU (l1 ⊔ l2)
  is-contr-map f = (y : B) → is-contr (fib f y)

Properties

Any contractible map is an equivalence

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

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

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

  isretr-map-inv-is-contr-map :
    (H : is-contr-map f) → ((map-inv-is-contr-map H) ∘ f) ~ id
  isretr-map-inv-is-contr-map H x =
    ap ( pr1 {B = λ z → (f z) ＝ (f x)})
       ( ( inv
           ( contraction
             ( H (f x))
             ( pair
               ( map-inv-is-contr-map H (f x))
               ( issec-map-inv-is-contr-map H (f x))))) ∙
         ( contraction (H (f x)) (pair x refl)))

  abstract
    is-equiv-is-contr-map : is-contr-map f → is-equiv f
    is-equiv-is-contr-map H =
      is-equiv-has-inverse
        ( map-inv-is-contr-map H)
        ( issec-map-inv-is-contr-map H)
        ( isretr-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}
  where

  abstract
    center-fib-is-coherently-invertible :
      is-coherently-invertible f → (y : B) → fib f y
    pr1 (center-fib-is-coherently-invertible H y) =
      inv-is-coherently-invertible H y
    pr2 (center-fib-is-coherently-invertible H y) =
      issec-inv-is-coherently-invertible H y

    contraction-fib-is-coherently-invertible :
      (H : is-coherently-invertible f) → (y : B) → (t : fib f y) →
      (center-fib-is-coherently-invertible H y) ＝ t
    contraction-fib-is-coherently-invertible H y (pair x refl) =
      eq-Eq-fib f y
        ( isretr-inv-is-coherently-invertible H x)
        ( ( right-unit) ∙
          ( inv ( coh-inv-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-fib-is-coherently-invertible H y
  pr2 (is-contr-map-is-coherently-invertible H y) =
    contraction-fib-is-coherently-invertible H y

Any equivalence is a contractible map

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

  abstract
    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

Agda-UniMath