From 6d164f10b1cfbc84c5ea853de2ffbeee8c06d598 Mon Sep 17 00:00:00 2001
From: Tom de Jong <tdejong.ac@gmail.com>
Date: Wed, 8 Nov 2023 10:04:59 +0000
Subject: [PATCH 1/3] Composition and left factor for epis/acyclic maps

---
 src/foundation/epimorphisms.lagda.md          | 19 +++++++++++++
 .../acyclic-maps.lagda.md                     | 28 +++++++++++++++++++
 2 files changed, 47 insertions(+)

diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md
index 5505581352..ad121fc73a 100644
--- a/src/foundation/epimorphisms.lagda.md
+++ b/src/foundation/epimorphisms.lagda.md
@@ -182,6 +182,25 @@ If the map `f : A → B` is epi, then its codiagonal is an equivalence.
   is-epimorphism-is-pushout = is-epimorphism-is-equiv-codiagonal-map
 ```
 
+### The class of epimorphisms is closed under composition and has the right cancellation property
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  (f : A → B) (g : B → C)
+  where
+
+  is-epimorphism-comp :
+    is-epimorphism f → is-epimorphism g → is-epimorphism (g ∘ f)
+  is-epimorphism-comp ef eg X =
+    is-emb-comp (precomp f X) (precomp g X) (ef X) (eg X)
+
+  is-epimorphism-left-factor :
+    is-epimorphism f → is-epimorphism (g ∘ f) → is-epimorphism g
+  is-epimorphism-left-factor ef ec X =
+    is-emb-right-factor (precomp f X) (precomp g X) (ef X) (ec X)
+```
+
 ## See also
 
 - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index a9f4aa9d5b..72dc4ae2ca 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -209,6 +209,34 @@ module _
       ( is-acyclic-map-is-epimorphism f e)
 ```
 
+### The class of acyclic maps is closed under composition and has the right cancellation property
+
+Since the acyclic maps are precisely the epimorphisms this follows from the
+corresponding facts about [epimorphisms](foundation.epimorphisms.md).
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  (f : A → B) (g : B → C)
+  where
+
+  is-acyclic-map-comp :
+    is-acyclic-map f → is-acyclic-map g → is-acyclic-map (g ∘ f)
+  is-acyclic-map-comp af ag =
+    is-acyclic-map-is-epimorphism (g ∘ f)
+      ( is-epimorphism-comp f g
+        ( is-epimorphism-is-acyclic-map f af)
+        ( is-epimorphism-is-acyclic-map g ag))
+
+  is-acyclic-map-left-factor :
+    is-acyclic-map f → is-acyclic-map (g ∘ f) → is-acyclic-map g
+  is-acyclic-map-left-factor af ac =
+    is-acyclic-map-is-epimorphism g
+      ( is-epimorphism-left-factor f g
+        ( is-epimorphism-is-acyclic-map f af)
+        ( is-epimorphism-is-acyclic-map (g ∘ f) ac))
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)

From 98d4c52380b5d04c470ac1b334c1b976df2db482 Mon Sep 17 00:00:00 2001
From: Tom de Jong <tdejong.ac@gmail.com>
Date: Thu, 9 Nov 2023 10:18:05 +0000
Subject: [PATCH 2/3] Swap arguments

---
 src/foundation/epimorphisms.lagda.md               |  6 +++---
 .../acyclic-maps.lagda.md                          | 14 +++++++-------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md
index ad121fc73a..17b3a19050 100644
--- a/src/foundation/epimorphisms.lagda.md
+++ b/src/foundation/epimorphisms.lagda.md
@@ -187,12 +187,12 @@ If the map `f : A → B` is epi, then its codiagonal is an equivalence.
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
-  (f : A → B) (g : B → C)
+  (g : B → C) (f : A → B)
   where
 
   is-epimorphism-comp :
-    is-epimorphism f → is-epimorphism g → is-epimorphism (g ∘ f)
-  is-epimorphism-comp ef eg X =
+    is-epimorphism g → is-epimorphism f → is-epimorphism (g ∘ f)
+  is-epimorphism-comp eg ef X =
     is-emb-comp (precomp f X) (precomp g X) (ef X) (eg X)
 
   is-epimorphism-left-factor :
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index 72dc4ae2ca..34ba5fb052 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -217,22 +217,22 @@ corresponding facts about [epimorphisms](foundation.epimorphisms.md).
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
-  (f : A → B) (g : B → C)
+  (g : B → C) (f : A → B)
   where
 
   is-acyclic-map-comp :
-    is-acyclic-map f → is-acyclic-map g → is-acyclic-map (g ∘ f)
-  is-acyclic-map-comp af ag =
+    is-acyclic-map g → is-acyclic-map f → is-acyclic-map (g ∘ f)
+  is-acyclic-map-comp ag af =
     is-acyclic-map-is-epimorphism (g ∘ f)
-      ( is-epimorphism-comp f g
-        ( is-epimorphism-is-acyclic-map f af)
-        ( is-epimorphism-is-acyclic-map g ag))
+      ( is-epimorphism-comp g f
+        ( is-epimorphism-is-acyclic-map g ag)
+        ( is-epimorphism-is-acyclic-map f af))
 
   is-acyclic-map-left-factor :
     is-acyclic-map f → is-acyclic-map (g ∘ f) → is-acyclic-map g
   is-acyclic-map-left-factor af ac =
     is-acyclic-map-is-epimorphism g
-      ( is-epimorphism-left-factor f g
+      ( is-epimorphism-left-factor g f
         ( is-epimorphism-is-acyclic-map f af)
         ( is-epimorphism-is-acyclic-map (g ∘ f) ac))
 ```

From 34829c409cc5823ec69b1927d76da6ea253a0423 Mon Sep 17 00:00:00 2001
From: Tom de Jong <tdejong.ac@gmail.com>
Date: Thu, 9 Nov 2023 11:37:47 +0000
Subject: [PATCH 3/3] More swapping

---
 src/foundation/epimorphisms.lagda.md                | 4 ++--
 src/synthetic-homotopy-theory/acyclic-maps.lagda.md | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md
index 17b3a19050..d3a14b661e 100644
--- a/src/foundation/epimorphisms.lagda.md
+++ b/src/foundation/epimorphisms.lagda.md
@@ -196,8 +196,8 @@ module _
     is-emb-comp (precomp f X) (precomp g X) (ef X) (eg X)
 
   is-epimorphism-left-factor :
-    is-epimorphism f → is-epimorphism (g ∘ f) → is-epimorphism g
-  is-epimorphism-left-factor ef ec X =
+    is-epimorphism (g ∘ f) → is-epimorphism f → is-epimorphism g
+  is-epimorphism-left-factor ec ef X =
     is-emb-right-factor (precomp f X) (precomp g X) (ef X) (ec X)
 ```
 
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index 34ba5fb052..bceb52e31a 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -229,12 +229,12 @@ module _
         ( is-epimorphism-is-acyclic-map f af))
 
   is-acyclic-map-left-factor :
-    is-acyclic-map f → is-acyclic-map (g ∘ f) → is-acyclic-map g
-  is-acyclic-map-left-factor af ac =
+    is-acyclic-map (g ∘ f) → is-acyclic-map f → is-acyclic-map g
+  is-acyclic-map-left-factor ac af =
     is-acyclic-map-is-epimorphism g
       ( is-epimorphism-left-factor g f
-        ( is-epimorphism-is-acyclic-map f af)
-        ( is-epimorphism-is-acyclic-map (g ∘ f) ac))
+        ( is-epimorphism-is-acyclic-map (g ∘ f) ac)
+        ( is-epimorphism-is-acyclic-map f af))
 ```
 
 ## See also