Merge branch 'master' into equality-iterated-sum-types

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}
+  (g : B → C) (f : A → B)
+  where
+
+  is-epimorphism-comp :
+    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 :
+    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)
+```
+
 ## See also
 
 - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)

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}
+  (g : B → C) (f : A → B)
+  where
+
+  is-acyclic-map-comp :
+    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 g f
+        ( is-epimorphism-is-acyclic-map g ag)
+        ( is-epimorphism-is-acyclic-map f af))
+
+  is-acyclic-map-left-factor :
+    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 (g ∘ f) ac)
+        ( is-epimorphism-is-acyclic-map f af))
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)

src/synthetic-homotopy-theory/acyclic-types.lagda.md

@@ -10,6 +10,7 @@ module synthetic-homotopy-theory.acyclic-types where
 open import foundation.contractible-types
 open import foundation.equivalences
 open import foundation.propositions
+open import foundation.retractions
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.functoriality-suspensions
@@ -54,6 +55,18 @@ is-acyclic-equiv' :
 is-acyclic-equiv' e = is-acyclic-equiv (inv-equiv e)
 ```
 
+### Acyclic types are closed under retracts
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-acyclic-retract-of : A retract-of B → is-acyclic B → is-acyclic A
+  is-acyclic-retract-of R ac =
+    is-contr-retract-of (suspension B) (retract-of-suspension-retract-of R) ac
+```
+
 ## See also
 
 ### Table of files related to cyclic types, groups, and rings