From e4b0e89667ae08b0de37d09268ac7131fa4dd905 Mon Sep 17 00:00:00 2001
From: Tom de Jong <43781735+tomdjong@users.noreply.github.com>
Date: Mon, 30 Oct 2023 15:29:57 +0000
Subject: [PATCH] The acyclic maps are exactly the epimorphisms (#894)

---
 .../acyclic-maps.lagda.md                     | 35 +++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index a19d58f7d3..dd2ae13ff5 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -7,11 +7,17 @@ module synthetic-homotopy-theory.acyclic-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.contractible-maps
+open import foundation.contractible-types
+open import foundation.epimorphisms
+open import foundation.equivalences
 open import foundation.fibers-of-maps
 open import foundation.propositions
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.acyclic-types
+open import synthetic-homotopy-theory.codiagonals-of-maps
+open import synthetic-homotopy-theory.suspensions-of-types
 ```
 
 </details>
@@ -41,6 +47,35 @@ module _
   is-prop-is-acyclic-map f = is-prop-type-Prop (is-acyclic-map-Prop f)
 ```
 
+## Properties
+
+### A map is acyclic if and only if it is an [epimorphism](foundation.epimorphisms.md)
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-acyclic-map-is-epimorphism : is-epimorphism f → is-acyclic-map f
+  is-acyclic-map-is-epimorphism e b =
+    is-contr-equiv
+      ( fiber (codiagonal-map f) b)
+      ( equiv-fiber-codiagonal-map-suspension-fiber f b)
+      ( is-contr-map-is-equiv
+        ( is-equiv-codiagonal-map-is-epimorphism f e)
+        ( b))
+
+  is-epimorphism-is-acyclic-map : is-acyclic-map f → is-epimorphism f
+  is-epimorphism-is-acyclic-map ac =
+    is-epimorphism-is-equiv-codiagonal-map f
+      ( is-equiv-is-contr-map
+        ( λ b →
+          is-contr-equiv
+            ( suspension (fiber f b))
+            ( inv-equiv (equiv-fiber-codiagonal-map-suspension-fiber f b))
+            ( ac b)))
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)