0-acyclic maps

Content created by Tom de Jong.

Created on 2023-12-01.
Last modified on 2023-12-01.

module synthetic-homotopy-theory.0-acyclic-maps where
open import foundation.epimorphisms-with-respect-to-sets
open import foundation.propositions
open import foundation.surjective-maps
open import foundation.truncation-levels
open import foundation.universe-levels

open import synthetic-homotopy-theory.truncated-acyclic-maps


A 0-acyclic map is a map whose fibers are 0-acyclic types, meaning that their suspension is 0-connected.

We can characterize the 0-acyclic maps as the surjective maps.


The predicate of being a 0-acyclic map

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

  is-0-acyclic-map-Prop : (A  B)  Prop (l1  l2)
  is-0-acyclic-map-Prop = is-truncated-acyclic-map-Prop (zero-𝕋)

  is-0-acyclic-map : (A  B)  UU (l1  l2)
  is-0-acyclic-map f = type-Prop (is-0-acyclic-map-Prop f)

  is-prop-is-0-acyclic-map :
    (f : A  B)  is-prop (is-0-acyclic-map f)
  is-prop-is-0-acyclic-map f =
    is-prop-type-Prop (is-0-acyclic-map-Prop f)


A map is 0-acyclic if and only if it is surjective

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

  is-surjective-is-0-acyclic-map :
    is-0-acyclic-map f  is-surjective f
  is-surjective-is-0-acyclic-map ac =
      ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type f ac)

  is-0-acyclic-map-is-surjective :
    is-surjective f  is-0-acyclic-map f
  is-0-acyclic-map-is-surjective s =
    is-truncated-acyclic-map-is-epimorphism-Truncated-Type f
      ( is-epimorphism-is-surjective-Set s)

See also

Recent changes