From 3dc09e83a088b432ac7796b11869ce384e28b1eb Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Tue, 10 Oct 2023 18:36:50 +0200
Subject: [PATCH] Dependent epimorphisms (#827)

This short PR adds the notion of dependent epimorphism to the library.
---
 src/foundation.lagda.md                       |  1 +
 .../dependent-epimorphisms.lagda.md           | 55 +++++++++++++++++++
 ...epimorphisms-with-respect-to-sets.lagda.md |  7 +++
 ...s-with-respect-to-truncated-types.lagda.md |  7 +++
 src/foundation/epimorphisms.lagda.md          | 20 +++++--
 .../acyclic-maps.lagda.md                     | 13 ++++-
 6 files changed, 96 insertions(+), 7 deletions(-)
 create mode 100644 src/foundation/dependent-epimorphisms.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 6f802ee511..cb4a973fb7 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -80,6 +80,7 @@ open import foundation.decidable-subtypes public
 open import foundation.decidable-types public
 open import foundation.dependent-binary-homotopies public
 open import foundation.dependent-binomial-theorem public
+open import foundation.dependent-epimorphisms public
 open import foundation.dependent-identifications public
 open import foundation.dependent-pair-types public
 open import foundation.descent-coproduct-types public
diff --git a/src/foundation/dependent-epimorphisms.lagda.md b/src/foundation/dependent-epimorphisms.lagda.md
new file mode 100644
index 0000000000..7174a357d7
--- /dev/null
+++ b/src/foundation/dependent-epimorphisms.lagda.md
@@ -0,0 +1,55 @@
+# Dependent epimorphisms
+
+```agda
+module foundation.dependent-epimorphisms where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-types
+open import foundation.universe-levels
+
+open import foundation-core.embeddings
+```
+
+</details>
+
+## Idea
+
+A **dependent epimorphism** is a map `f : A → B` such that the precomposition
+function
+
+```text
+  - ∘ f : ((b : B) → C b) → ((a : A) → C (f a))
+```
+
+is an [embedding](foundation-core.embeddings.md) for every type family `C` over
+`B`.
+
+Clearly, every dependent epimorphism is an
+[epimorphism](foundation.epimorphisms.md). The converse is also true, i.e.,
+every epimorphism is a dependent epimorphism. Therefore it follows that a map
+`f : A → B` is [acyclic](synthetic-homotopy-theory.acyclic-maps.md) if and only
+if it is an epimorphism, if and only if it is a dependent epimorphism.
+
+## Definitions
+
+### The predicate of being a dependent epimorphism
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-dependent-epimorphism : (A → B) → UUω
+  is-dependent-epimorphism f =
+    {l : Level} (C : B → UU l) → is-emb (precomp-Π f C)
+```
+
+## See also
+
+- [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
+- [Epimorphisms](foundation.epimorphisms.md)
+- [Epimorphisms with respect to sets](foundation.epimorphisms-with-respect-to-sets.md)
+- [Epimorphisms with respect to truncated types](foundation.epimorphisms-with-respect-to-truncated-types.md)
diff --git a/src/foundation/epimorphisms-with-respect-to-sets.lagda.md b/src/foundation/epimorphisms-with-respect-to-sets.lagda.md
index fa8cb45190..59df999c3b 100644
--- a/src/foundation/epimorphisms-with-respect-to-sets.lagda.md
+++ b/src/foundation/epimorphisms-with-respect-to-sets.lagda.md
@@ -97,3 +97,10 @@ abstract
     h : B → Prop (l1 ⊔ l2)
     h y = ∃-Prop A (λ x → f x ＝ y)
 ```
+
+## See also
+
+- [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
+- [Dependent epimorphisms](foundation.dependent-epimorphisms.md)
+- [Epimorphisms](foundation.epimorphisms.md)
+- [Epimorphisms with respect to truncated types](foundation.epimorphisms-with-respect-to-truncated-types.md)
diff --git a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
index 95ad386355..fe4612e3dc 100644
--- a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
+++ b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
@@ -110,3 +110,10 @@ module _
       ( is-truncation-trunc X)
       ( H X)
 ```
+
+## See also
+
+- [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
+- [Dependent epimorphisms](foundation.dependent-epimorphisms.md)
+- [Epimorphisms](foundation.epimorphisms.md)
+- [Epimorphisms with respect to sets](foundation.epimorphisms-with-respect-to-sets.md)
diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md
index 6aad49ca89..701132c370 100644
--- a/src/foundation/epimorphisms.lagda.md
+++ b/src/foundation/epimorphisms.lagda.md
@@ -24,13 +24,23 @@ function
   - ∘ f : (B → X) → (A → X)
 ```
 
-is an embedding for every type `X`.
+is an [embedding](foundation-core.embeddings.md) for every type `X`.
 
 ## Definitions
 
 ```agda
-is-epimorphism :
-  {l1 l2 : Level} (l : Level) {A : UU l1} {B : UU l2} →
-  (A → B) → UU (l1 ⊔ l2 ⊔ lsuc l)
-is-epimorphism l f = (X : UU l) → is-emb (precomp f X)
+module _
+  {l1 l2 : Level} (l : Level) {A : UU l1} {B : UU l2}
+  where
+
+  is-epimorphism : (A → B) → UUω
+  is-epimorphism f = {l : Level} (X : UU l) → is-emb (precomp f X)
 ```
+
+## See also
+
+- [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
+- [Dependent epimorphisms](foundation.dependent-epimorphisms.md)
+- [Epimorphisms](foundation.epimorphisms.md)
+- [Epimorphisms with respect to sets](foundation.epimorphisms-with-respect-to-sets.md)
+- [Epimorphisms with respect to truncated types](foundation.epimorphisms-with-respect-to-truncated-types.md)
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index dbaef401e0..a19d58f7d3 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -18,9 +18,13 @@ open import synthetic-homotopy-theory.acyclic-types
 
 ## Idea
 
-A map `f : A → B` is said to be **acyclic** if its fibers are acyclic types.
+A map `f : A → B` is said to be **acyclic** if its
+[fibers](foundation-core.fibers-of-maps.md) are
+[acyclic types](synthetic-homotopy-theory.acyclic-types.md).
 
-## Definition
+## Definitions
+
+### The predicate of being an acyclic map
 
 ```agda
 module _
@@ -39,6 +43,11 @@ module _
 
 ## See also
 
+- [Dependent epimorphisms](foundation.dependent-epimorphisms.md)
+- [Epimorphisms](foundation.epimorphisms.md)
+- [Epimorphisms with respect to sets](foundation.epimorphisms-with-respect-to-sets.md)
+- [Epimorphisms with respect to truncated types](foundation.epimorphisms-with-respect-to-truncated-types.md)
+
 ### Table of files related to cyclic types, groups, and rings
 
 {{#include tables/cyclic-types.md}}