From fe41f7e990b9332c2d8c74ee6b8ffe2bc87ae97e Mon Sep 17 00:00:00 2001
From: Tom de Jong <43781735+tomdjong@users.noreply.github.com>
Date: Mon, 27 Nov 2023 17:19:45 +0100
Subject: [PATCH] A map is `k`-acyclic iff it is a `k`-epi iff it is a
dependent `k`-epi (#949)
---
src/foundation.lagda.md | 1 +
...s-with-respect-to-truncated-types.lagda.md | 79 ++++++
.../dependent-epimorphisms.lagda.md | 4 +-
src/synthetic-homotopy-theory.lagda.md | 1 +
.../truncated-acyclic-maps.lagda.md | 260 ++++++++++++++++++
5 files changed, 343 insertions(+), 2 deletions(-)
create mode 100644 src/foundation/dependent-epimorphisms-with-respect-to-truncated-types.lagda.md
create mode 100644 src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index d7d0deca0a..2209686ed5 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -85,6 +85,7 @@ 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-epimorphisms-with-respect-to-truncated-types public
open import foundation.dependent-homotopies public
open import foundation.dependent-identifications public
open import foundation.dependent-pair-types public
diff --git a/src/foundation/dependent-epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/dependent-epimorphisms-with-respect-to-truncated-types.lagda.md
new file mode 100644
index 0000000000..7e107654bd
--- /dev/null
+++ b/src/foundation/dependent-epimorphisms-with-respect-to-truncated-types.lagda.md
@@ -0,0 +1,79 @@
+# Dependent epimorphisms with respect to truncated types
+
+```agda
+module foundation.dependent-epimorphisms-with-respect-to-truncated-types where
+```
+
+Imports
+
+```agda
+open import foundation.epimorphisms-with-respect-to-truncated-types
+open import foundation.universe-levels
+
+open import foundation-core.embeddings
+open import foundation-core.precomposition-dependent-functions
+open import foundation-core.truncated-types
+open import foundation-core.truncation-levels
+```
+
+
+
+## Idea
+
+A **dependent `k`-epimorphism** is a map `f : A → B` such that the
+[precomposition function](foundation.precomposition-dependent-functions.md)
+
+```text
+ - ∘ f : ((b : B) → C b) → ((a : A) → C (f a))
+```
+
+is an [embedding](foundation-core.embeddings.md) for every family `C` of
+[`k`-types](foundation.truncated-types.md) over `B`.
+
+Clearly, every dependent `k`-epimorphism is a
+[`k`-epimorphism](foundation.epimorphisms-with-respect-to-truncated-types.md).
+The converse is also true, i.e., every `k`-epimorphism is a dependent
+`k`-epimorphism. Therefore it follows that a map `f : A → B` is
+[`k`-acyclic](synthetic-homotopy-theory.truncated-acyclic-maps.md) if and only
+if it is a `k`-epimorphism, if and only if it is a dependent `k`-epimorphism.
+
+## Definitions
+
+### The predicate of being a dependent `k`-epimorphism
+
+```agda
+module _
+ {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
+ where
+
+ is-dependent-epimorphism-Truncated-Type : (A → B) → UUω
+ is-dependent-epimorphism-Truncated-Type f =
+ {l : Level} (C : B → Truncated-Type l k) →
+ is-emb (precomp-Π f (λ b → type-Truncated-Type (C b)))
+```
+
+## Properties
+
+### Every dependent `k`-epimorphism is a `k`-epimorphism
+
+```agda
+module _
+ {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+ where
+
+ is-epimorphism-is-dependent-epimorphism-Truncated-Type :
+ is-dependent-epimorphism-Truncated-Type k f →
+ is-epimorphism-Truncated-Type k f
+ is-epimorphism-is-dependent-epimorphism-Truncated-Type e X = e (λ _ → X)
+```
+
+The converse of the above, that every `k`-epimorphism is a dependent
+`k`-epimorphism, can be found in the file on
+[`k`-acyclic maps](synthetic-homotopy-theory.truncated-acyclic-maps.md).
+
+## See also
+
+- [`k`-acyclic maps](synthetic-homotopy-theory.truncated-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/dependent-epimorphisms.lagda.md b/src/foundation/dependent-epimorphisms.lagda.md
index 46d853b996..d4da0dd5e6 100644
--- a/src/foundation/dependent-epimorphisms.lagda.md
+++ b/src/foundation/dependent-epimorphisms.lagda.md
@@ -18,8 +18,8 @@ open import foundation-core.precomposition-dependent-functions
## Idea
-A **dependent epimorphism** is a map `f : A → B` such that the precomposition
-function
+A **dependent epimorphism** is a map `f : A → B` such that the
+[precomposition function](foundation.precomposition-dependent-functions.md)
```text
- ∘ f : ((b : B) → C b) → ((a : A) → C (f a))
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index cf3dc9f7ce..23daf56cec 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -84,6 +84,7 @@ open import synthetic-homotopy-theory.suspensions-of-pointed-types public
open import synthetic-homotopy-theory.suspensions-of-types public
open import synthetic-homotopy-theory.tangent-spheres public
open import synthetic-homotopy-theory.triple-loop-spaces public
+open import synthetic-homotopy-theory.truncated-acyclic-maps public
open import synthetic-homotopy-theory.truncated-acyclic-types public
open import synthetic-homotopy-theory.universal-cover-circle public
open import synthetic-homotopy-theory.universal-property-circle public
diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
new file mode 100644
index 0000000000..3ddb1258b0
--- /dev/null
+++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
@@ -0,0 +1,260 @@
+# `k`-acyclic maps
+
+```agda
+module synthetic-homotopy-theory.truncated-acyclic-maps where
+```
+
+Imports
+
+```agda
+open import foundation.connected-maps
+open import foundation.connected-types
+open import foundation.constant-maps
+open import foundation.dependent-epimorphisms-with-respect-to-truncated-types
+open import foundation.dependent-pair-types
+open import foundation.dependent-universal-property-equivalences
+open import foundation.embeddings
+open import foundation.epimorphisms-with-respect-to-truncated-types
+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.precomposition-dependent-functions
+open import foundation.precomposition-functions
+open import foundation.propositions
+open import foundation.truncated-types
+open import foundation.truncation-levels
+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.codiagonals-of-maps
+open import synthetic-homotopy-theory.suspensions-of-types
+open import synthetic-homotopy-theory.truncated-acyclic-types
+```
+
+
+
+## Idea
+
+A map `f : A → B` is said to be **`k`-acyclic** if its
+[fibers](foundation-core.fibers-of-maps.md) are
+[`k`-acyclic types](synthetic-homotopy-theory.truncated-acyclic-types.md).
+
+## Definitions
+
+### The predicate of being a `k`-acyclic map
+
+```agda
+module _
+ {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
+ where
+
+ is-truncated-acyclic-map-Prop : (A → B) → Prop (l1 ⊔ l2)
+ is-truncated-acyclic-map-Prop f =
+ Π-Prop B (λ b → is-truncated-acyclic-Prop k (fiber f b))
+
+ is-truncated-acyclic-map : (A → B) → UU (l1 ⊔ l2)
+ is-truncated-acyclic-map f = type-Prop (is-truncated-acyclic-map-Prop f)
+
+ is-prop-is-truncated-acyclic-map :
+ (f : A → B) → is-prop (is-truncated-acyclic-map f)
+ is-prop-is-truncated-acyclic-map f =
+ is-prop-type-Prop (is-truncated-acyclic-map-Prop f)
+```
+
+## Properties
+
+### A map is `k`-acyclic if and only if it is an [epimorphism with respect to `k`-types](foundation.epimorphisms-with-respect-to-truncated-types.md)
+
+```agda
+module _
+ {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+ where
+
+ is-truncated-acyclic-map-is-epimorphism-Truncated-Type :
+ is-epimorphism-Truncated-Type k f → is-truncated-acyclic-map k f
+ is-truncated-acyclic-map-is-epimorphism-Truncated-Type e b =
+ is-connected-equiv
+ ( equiv-fiber-codiagonal-map-suspension-fiber f b)
+ ( is-connected-codiagonal-map-is-epimorphism-Truncated-Type k f e b)
+
+ is-epimorphism-is-truncated-acyclic-map-Truncated-Type :
+ is-truncated-acyclic-map k f → is-epimorphism-Truncated-Type k f
+ is-epimorphism-is-truncated-acyclic-map-Truncated-Type ac =
+ is-epimorphism-is-connected-codiagonal-map-Truncated-Type k f
+ ( λ b →
+ is-connected-equiv'
+ ( equiv-fiber-codiagonal-map-suspension-fiber f b)
+ ( ac b))
+```
+
+### A type is `k`-acyclic if and only if its terminal map is a `k`-acyclic map
+
+```agda
+module _
+ {l : Level} {k : 𝕋} (A : UU l)
+ where
+
+ is-truncated-acyclic-map-terminal-map-is-truncated-acyclic :
+ is-truncated-acyclic k A →
+ is-truncated-acyclic-map k (terminal-map {A = A})
+ is-truncated-acyclic-map-terminal-map-is-truncated-acyclic ac u =
+ is-truncated-acyclic-equiv (equiv-fiber-terminal-map u) ac
+
+ is-truncated-acyclic-is-truncated-acyclic-map-terminal-map :
+ is-truncated-acyclic-map k (terminal-map {A = A}) →
+ is-truncated-acyclic k A
+ is-truncated-acyclic-is-truncated-acyclic-map-terminal-map ac =
+ is-truncated-acyclic-equiv inv-equiv-fiber-terminal-map-star (ac star)
+```
+
+### A type is `k`-acyclic if and only if the constant map from any `k`-type is an embedding
+
+More precisely, `A` is `k`-acyclic if and only if for all `k`-types `X`, the map
+
+```text
+ const : X → (A → X)
+```
+
+is an embedding.
+
+```agda
+module _
+ {l : Level} {k : 𝕋} (A : UU l)
+ where
+
+ is-emb-const-is-truncated-acyclic-Truncated-Type :
+ is-truncated-acyclic k A →
+ {l' : Level} (X : Truncated-Type l' k) →
+ is-emb (const A (type-Truncated-Type X))
+ is-emb-const-is-truncated-acyclic-Truncated-Type ac X =
+ is-emb-comp
+ ( precomp terminal-map (type-Truncated-Type X))
+ ( map-inv-left-unit-law-function-type (type-Truncated-Type X))
+ ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type terminal-map
+ ( is-truncated-acyclic-map-terminal-map-is-truncated-acyclic A ac)
+ ( X))
+ ( is-emb-is-equiv
+ ( is-equiv-map-inv-left-unit-law-function-type (type-Truncated-Type X)))
+
+ is-truncated-acyclic-is-emb-const-Truncated-Type :
+ ({l' : Level} (X : Truncated-Type l' k) →
+ is-emb (const A (type-Truncated-Type X))) →
+ is-truncated-acyclic k A
+ is-truncated-acyclic-is-emb-const-Truncated-Type e =
+ is-truncated-acyclic-is-truncated-acyclic-map-terminal-map A
+ ( is-truncated-acyclic-map-is-epimorphism-Truncated-Type
+ ( terminal-map)
+ ( λ X →
+ is-emb-triangle-is-equiv'
+ ( const A (type-Truncated-Type X))
+ ( precomp terminal-map (type-Truncated-Type X))
+ ( map-inv-left-unit-law-function-type (type-Truncated-Type X))
+ ( refl-htpy)
+ ( is-equiv-map-inv-left-unit-law-function-type
+ ( type-Truncated-Type X))
+ ( e X)))
+```
+
+### A map is `k`-acyclic if and only if it is an [dependent `k`-epimorphism](foundation.dependent-epimorphisms-with-respect-to-truncated-types.md)
+
+The proof is similar to that of dependent epimorphisms and
+[acyclic-maps](synthetic-homotopy-theory.acyclic-maps.md).
+
+```agda
+module _
+ {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+ where
+
+ is-truncated-acyclic-map-is-dependent-epimorphism-Truncated-Type :
+ is-dependent-epimorphism-Truncated-Type k f → is-truncated-acyclic-map k f
+ is-truncated-acyclic-map-is-dependent-epimorphism-Truncated-Type e =
+ is-truncated-acyclic-map-is-epimorphism-Truncated-Type f
+ ( is-epimorphism-is-dependent-epimorphism-Truncated-Type f e)
+
+ is-dependent-epimorphism-is-truncated-acyclic-map-Truncated-Type :
+ is-truncated-acyclic-map k f → is-dependent-epimorphism-Truncated-Type k f
+ is-dependent-epimorphism-is-truncated-acyclic-map-Truncated-Type ac C =
+ is-emb-comp
+ ( precomp-Π
+ ( map-inv-equiv-total-fiber f)
+ ( type-Truncated-Type ∘ C ∘ pr1) ∘ ind-Σ)
+ ( map-Π (λ b → const (fiber f b) (type-Truncated-Type (C b))))
+ ( is-emb-comp
+ ( precomp-Π
+ ( map-inv-equiv-total-fiber f)
+ ( type-Truncated-Type ∘ C ∘ pr1))
+ ( ind-Σ)
+ ( is-emb-is-equiv
+ ( is-equiv-precomp-Π-is-equiv
+ ( is-equiv-map-inv-equiv-total-fiber f)
+ (type-Truncated-Type ∘ C ∘ pr1)))
+ ( is-emb-is-equiv is-equiv-ind-Σ))
+ ( is-emb-map-Π
+ ( λ b →
+ is-emb-const-is-truncated-acyclic-Truncated-Type
+ ( fiber f b)
+ ( ac b)
+ ( C b)))
+```
+
+In particular, every `k`-epimorphism is actually a dependent `k`-epimorphism.
+
+```agda
+module _
+ {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+ where
+
+ is-dependent-epimorphism-is-epimorphism-Truncated-Type :
+ is-epimorphism-Truncated-Type k f →
+ is-dependent-epimorphism-Truncated-Type k f
+ is-dependent-epimorphism-is-epimorphism-Truncated-Type e =
+ is-dependent-epimorphism-is-truncated-acyclic-map-Truncated-Type f
+ ( is-truncated-acyclic-map-is-epimorphism-Truncated-Type f e)
+```
+
+### The class of `k`-acyclic maps is closed under composition and has the right cancellation property
+
+Since the `k`-acyclic maps are precisely the `k`-epimorphisms this follows from
+the corresponding facts about
+[`k`-epimorphisms](foundation.epimorphisms-with-respect-to-truncated-types.md).
+
+```agda
+module _
+ {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {C : UU l3}
+ (g : B → C) (f : A → B)
+ where
+
+ is-truncated-acyclic-map-comp :
+ is-truncated-acyclic-map k g →
+ is-truncated-acyclic-map k f →
+ is-truncated-acyclic-map k (g ∘ f)
+ is-truncated-acyclic-map-comp ag af =
+ is-truncated-acyclic-map-is-epimorphism-Truncated-Type (g ∘ f)
+ ( is-epimorphism-comp-Truncated-Type k g f
+ ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type g ag)
+ ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type f af))
+
+ is-truncated-acyclic-map-left-factor :
+ is-truncated-acyclic-map k (g ∘ f) →
+ is-truncated-acyclic-map k f →
+ is-truncated-acyclic-map k g
+ is-truncated-acyclic-map-left-factor ac af =
+ is-truncated-acyclic-map-is-epimorphism-Truncated-Type g
+ ( is-epimorphism-left-factor-Truncated-Type k g f
+ ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type (g ∘ f) ac)
+ ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type f af))
+```
+
+## See also
+
+- [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
+- [Acyclic types](synthetic-homotopy-theory.acyclic-types.md)
+- [`k`-acyclic types](synthetic-homotopy-theory.truncated-acyclic-types.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)