A map is a dependent epi iff it is an epi iff it is acyclic

src/foundation/dependent-epimorphisms.lagda.md

@@ -7,6 +7,7 @@ module foundation.dependent-epimorphisms where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.epimorphisms
 open import foundation.function-types
 open import foundation.universe-levels
 
@@ -47,6 +48,24 @@ module _
     {l : Level} (C : B → UU l) → is-emb (precomp-Π f C)
 ```
 
+## Properties
+
+### Every dependent epimorphism is an epimorphism
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-epimorphism-is-dependent-epimorphism :
+    is-dependent-epimorphism f → is-epimorphism f
+  is-epimorphism-is-dependent-epimorphism e X = e (λ _ → X)
+```
+
+The converse of the above, that every epimorphism is a dependent epimorphism,
+can be found in the file on
+[acyclic maps](synthetic-homotopy-theory.acyclic-maps.md).
+
 ## See also
 
 - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)

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

@@ -7,13 +7,22 @@ module synthetic-homotopy-theory.acyclic-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.constant-maps
 open import foundation.contractible-maps
 open import foundation.contractible-types
+open import foundation.dependent-epimorphisms
+open import foundation.dependent-pair-types
+open import foundation.embeddings
 open import foundation.epimorphisms
 open import foundation.equivalences
 open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.homotopies
 open import foundation.propositions
+open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
+open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.acyclic-types
@@ -95,6 +104,111 @@ module _
     is-acyclic-equiv inv-equiv-fiber-terminal-map-star (ac star)
 ```
 
+### A type is acyclic if and only if the constant map from any type is an embedding
+
+More precisely, `A` is acyclic if and only if for all types `X`, the map
+
+```text
+ const : X → (A → X)
+```
+
+is an embedding.
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  is-emb-const-is-acyclic :
+    is-acyclic A →
+    {l' : Level} (X : UU l') → is-emb (const A X)
+  is-emb-const-is-acyclic ac X =
+    is-emb-comp
+      ( precomp terminal-map X)
+      ( map-inv-left-unit-law-function-type X)
+      ( is-epimorphism-is-acyclic-map terminal-map
+        ( is-acyclic-map-terminal-map-is-acyclic A ac)
+        ( X))
+      ( is-emb-is-equiv (is-equiv-map-inv-left-unit-law-function-type X))
+
+  is-acyclic-is-emb-const :
+    ({l' : Level} (X : UU l') → is-emb (const A X)) →
+    is-acyclic A
+  is-acyclic-is-emb-const e =
+    is-acyclic-is-acyclic-map-terminal-map A
+      ( is-acyclic-map-is-epimorphism
+        ( terminal-map)
+        ( λ X →
+          is-emb-triangle-is-equiv'
+            ( const A X)
+            ( precomp terminal-map X)
+            ( map-inv-left-unit-law-function-type X)
+            ( refl-htpy)
+            ( is-equiv-map-inv-left-unit-law-function-type X)
+            ( e X)))
+```
+
+### A map is acyclic if and only if it is an [dependent epimorphism](foundation.dependent-epimorphisms.md)
+
+The following diagram is a helpful illustration in the second proof:
+
+```text
+                        precomp f
+       (b : B) → C b ------------- > (a : A) → C (f a)
+             |                               ^
+             |                               |
+ map-Π const |                               | ≃ [precomp with the equivalence
+             |                               |        A ≃ Σ B (fiber f)     ]
+             v               ind-Σ           |
+ ((b : B) → fiber f b → C b) ----> (s : Σ B (fiber f)) → C (pr1 s)
+                              ≃
+                          [currying]
+```
+
+The left map is an embedding if f is an acyclic map, because const is an
+embedding in this case.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-acyclic-map-is-dependent-epimorphism :
+    is-dependent-epimorphism f → is-acyclic-map f
+  is-acyclic-map-is-dependent-epimorphism e =
+    is-acyclic-map-is-epimorphism f
+      ( is-epimorphism-is-dependent-epimorphism f e)
+
+  is-dependent-epimorphism-is-acyclic-map :
+    is-acyclic-map f → is-dependent-epimorphism f
+  is-dependent-epimorphism-is-acyclic-map ac C =
+    is-emb-comp
+      ( precomp-Π (map-inv-equiv-total-fiber f) (C ∘ pr1) ∘ ind-Σ)
+      ( map-Π (λ b → const (fiber f b) (C b)))
+      ( is-emb-comp
+        ( precomp-Π (map-inv-equiv-total-fiber f) (C ∘ pr1))
+        ( ind-Σ)
+        ( is-emb-is-equiv
+          ( is-equiv-precomp-Π-is-equiv
+            ( is-equiv-map-inv-equiv-total-fiber f) (C ∘ pr1)))
+        ( is-emb-is-equiv is-equiv-ind-Σ))
+      ( is-emb-map-Π (λ b → is-emb-const-is-acyclic (fiber f b) (ac b) (C b)))
+```
+
+In particular, every epimorphism is actually a dependent epimorphism.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-dependent-epimorphism-is-epimorphism :
+    is-epimorphism f → is-dependent-epimorphism f
+  is-dependent-epimorphism-is-epimorphism e =
+    is-dependent-epimorphism-is-acyclic-map f
+      ( is-acyclic-map-is-epimorphism f e)
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)