Cofibers

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

Created on 2022-05-13.
Last modified on 2023-06-28.

module synthetic-homotopy-theory.cofibers where
Imports 
open import foundation.constant-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.unit-type
open import foundation.universe-levels

open import structured-types.pointed-types

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.universal-property-pushouts

Idea

The cofiber of a map f : A → B is the pushout of the span 1 ← A → B.

Definitions

The cofiber of a map

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

  cofiber : (A → B) → UU (l1 ⊔ l2)
  cofiber f = pushout f (const A unit star)

  cocone-cofiber :
    (f : A → B) → cocone f (const A unit star) (cofiber f)
  cocone-cofiber f = cocone-pushout f (const A unit star)

  inl-cofiber : (f : A → B) → B → cofiber f
  inl-cofiber f = pr1 (cocone-cofiber f)

  inr-cofiber : (f : A → B) → unit → cofiber f
  inr-cofiber f = pr1 (pr2 (cocone-cofiber f))

  point-cofiber : (f : A → B) → cofiber f
  point-cofiber f = inr-cofiber f star

  cofiber-Pointed-Type : (f : A → B) → Pointed-Type (l1 ⊔ l2)
  pr1 (cofiber-Pointed-Type f) = cofiber f
  pr2 (cofiber-Pointed-Type f) = point-cofiber f

  universal-property-cofiber :
    (f : A → B) {l : Level} →
    universal-property-pushout l f (const A unit star) (cocone-cofiber f)
  universal-property-cofiber f = up-pushout f (const A unit star)

Properties

The cofiber of an equivalence is contractible

Note that this is not a logical equivalence. Not every map whose cofibers are all contractible is an equivalence. For instance, the cofiber of X → 1 where X is an acyclic type is by definition contractible. Examples of noncontractible acyclic types include Hatcher's acyclic type.

is-contr-cofiber-is-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-equiv f → is-contr (cofiber f)
is-contr-cofiber-is-equiv {A = A} f is-equiv-f =
  is-contr-is-equiv'
    ( unit)
    ( pr1 (pr2 (cocone-cofiber f)))
    ( is-equiv-universal-property-pushout
      ( f)
      ( const A unit star)
      ( cocone-cofiber f)
      ( is-equiv-f)
      ( universal-property-cofiber f))
    ( is-contr-unit)

The cofiber of the point inclusion of X is equivalent to X

is-equiv-inl-cofiber-point :
  {l : Level} {B : UU l} (b : B) → is-equiv (inl-cofiber (point b))
is-equiv-inl-cofiber-point {B = B} b =
  is-equiv-universal-property-pushout'
    ( const unit B b)
    ( const unit unit star)
    ( cocone-pushout (const unit B b) (const unit unit star))
    ( is-equiv-is-contr (const unit unit star) is-contr-unit is-contr-unit)
    ( up-pushout (const unit B b) (const unit unit star))

Recent changes