# 0-acyclic maps

Content created by Tom de Jong.

Created on 2023-12-01.

module synthetic-homotopy-theory.0-acyclic-maps where

Imports
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


## Idea

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.

## Definition

### The predicate of being a 0-acyclic map

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

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)


## Properties

### 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)
where

is-surjective-is-0-acyclic-map :
is-0-acyclic-map f → is-surjective f
is-surjective-is-0-acyclic-map ac =
is-surjective-is-epimorphism-Set
( 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)