From e9fad24575d58d69c53704c56f3dee8960f2a55b Mon Sep 17 00:00:00 2001 From: Tom de Jong Date: Tue, 7 Nov 2023 17:25:52 +0000 Subject: [PATCH 1/5] Every dependent epimorphism is an epimorphism --- src/foundation/dependent-epimorphisms.lagda.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/foundation/dependent-epimorphisms.lagda.md b/src/foundation/dependent-epimorphisms.lagda.md index 7174a357d7..847f3f3d8b 100644 --- a/src/foundation/dependent-epimorphisms.lagda.md +++ b/src/foundation/dependent-epimorphisms.lagda.md @@ -7,6 +7,7 @@ module foundation.dependent-epimorphisms where
Imports ```agda +open import foundation.epimorphisms open import foundation.function-types open import foundation.universe-levels @@ -47,6 +48,20 @@ 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) +``` + ## See also - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md) From 80abb2165644fe21b0894927a61d766414c4a4ad Mon Sep 17 00:00:00 2001 From: Tom de Jong Date: Tue, 7 Nov 2023 17:26:13 +0000 Subject: [PATCH 2/5] Dependent epi = epi = acyclic --- .../acyclic-maps.lagda.md | 114 ++++++++++++++++++ 1 file changed, 114 insertions(+) diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 77b7d88bfa..5bb7514e91 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -7,13 +7,22 @@ module synthetic-homotopy-theory.acyclic-maps where
Imports ```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) From 79f4a6c29a46805c65f5103fe040316c4be81390 Mon Sep 17 00:00:00 2001 From: Tom de Jong Date: Tue, 7 Nov 2023 17:43:59 +0000 Subject: [PATCH 3/5] Arrow at the end of the line --- src/synthetic-homotopy-theory/acyclic-maps.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 5bb7514e91..a9f4aa9d5b 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -132,8 +132,8 @@ module _ ( 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 + ({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 From 2cdc4b53d9359caf40fe28b09bf9952516fae728 Mon Sep 17 00:00:00 2001 From: Tom de Jong Date: Tue, 7 Nov 2023 17:46:15 +0000 Subject: [PATCH 4/5] Pointer to epi->dep-epi --- src/foundation/dependent-epimorphisms.lagda.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/foundation/dependent-epimorphisms.lagda.md b/src/foundation/dependent-epimorphisms.lagda.md index 847f3f3d8b..b9d34cc836 100644 --- a/src/foundation/dependent-epimorphisms.lagda.md +++ b/src/foundation/dependent-epimorphisms.lagda.md @@ -62,6 +62,9 @@ module _ 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) From d264800504cda775b162f9b6f32c8384fec73396 Mon Sep 17 00:00:00 2001 From: Tom de Jong Date: Tue, 7 Nov 2023 17:49:35 +0000 Subject: [PATCH 5/5] Fix overflowing line --- src/foundation/dependent-epimorphisms.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/foundation/dependent-epimorphisms.lagda.md b/src/foundation/dependent-epimorphisms.lagda.md index b9d34cc836..d828c9a1e2 100644 --- a/src/foundation/dependent-epimorphisms.lagda.md +++ b/src/foundation/dependent-epimorphisms.lagda.md @@ -63,7 +63,8 @@ module _ ``` 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). +can be found in the file on +[acyclic maps](synthetic-homotopy-theory.acyclic-maps.md). ## See also