From 9743045576f0c8f392359ddbedf78757472077d9 Mon Sep 17 00:00:00 2001 From: Tom de Jong <43781735+tomdjong@users.noreply.github.com> Date: Sun, 29 Oct 2023 20:44:11 +0000 Subject: [PATCH 1/3] Codiagonal is fiberwise suspension (#892) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This will be used in an upcoming PR that characterizes the epimorphisms as the acyclic maps. --------- Co-authored-by: Fredrik Bakke Co-authored-by: Vojtěch Štěpančík --- .../codiagonals-of-maps.lagda.md | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md b/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md index 43c4806753..3ee72e31a9 100644 --- a/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md +++ b/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md @@ -7,13 +7,23 @@ module synthetic-homotopy-theory.codiagonals-of-maps where
Imports ```agda +open import foundation.contractible-maps +open import foundation.contractible-types open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.fibers-of-maps open import foundation.function-types open import foundation.homotopies +open import foundation.propositions +open import foundation.unit-type open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.pushouts +open import synthetic-homotopy-theory.suspension-structures +open import synthetic-homotopy-theory.suspensions-of-types +open import synthetic-homotopy-theory.universal-property-pushouts +open import synthetic-homotopy-theory.universal-property-suspensions ```
@@ -69,3 +79,80 @@ module _ compute-glue-codiagonal-map = compute-glue-cogap f f cocone-codiagonal-map ``` + +## Properties + +### The codiagonal is the fiberwise suspension + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (b : B) + where + + universal-property-suspension-cocone-fiber : + {l : Level} → + Σ ( cocone terminal-map terminal-map (fiber (codiagonal-map f) b)) + ( universal-property-pushout l terminal-map terminal-map) + universal-property-suspension-cocone-fiber = + universal-property-pushout-cogap-fiber-up-to-equiv f f + ( cocone-codiagonal-map f) + ( b) + ( fiber f b) + ( unit) + ( unit) + ( inv-equiv + ( terminal-map , + ( is-equiv-terminal-map-is-contr (is-torsorial-path' b)))) + ( inv-equiv + ( terminal-map , + ( is-equiv-terminal-map-is-contr (is-torsorial-path' b)))) + ( id-equiv) + ( terminal-map) + ( terminal-map) + ( λ _ → eq-is-contr (is-torsorial-path' b)) + ( λ _ → eq-is-contr (is-torsorial-path' b)) + + suspension-cocone-fiber : + suspension-cocone (fiber f b) (fiber (codiagonal-map f) b) + suspension-cocone-fiber = + pr1 (universal-property-suspension-cocone-fiber {lzero}) + + universal-property-suspension-fiber : + {l : Level} → + universal-property-pushout l + ( terminal-map) + ( terminal-map) + ( suspension-cocone-fiber) + universal-property-suspension-fiber = + pr2 universal-property-suspension-cocone-fiber + + fiber-codiagonal-map-suspension-fiber : + suspension (fiber f b) → fiber (codiagonal-map f) b + fiber-codiagonal-map-suspension-fiber = + cogap terminal-map terminal-map suspension-cocone-fiber + + is-equiv-fiber-codiagonal-map-suspension-fiber : + is-equiv fiber-codiagonal-map-suspension-fiber + is-equiv-fiber-codiagonal-map-suspension-fiber = + is-equiv-up-pushout-up-pushout + ( terminal-map) + ( terminal-map) + ( cocone-pushout terminal-map terminal-map) + ( suspension-cocone-fiber) + ( cogap terminal-map terminal-map (suspension-cocone-fiber)) + ( htpy-cocone-map-universal-property-pushout + ( terminal-map) + ( terminal-map) + ( cocone-pushout terminal-map terminal-map) + ( up-pushout terminal-map terminal-map) + ( suspension-cocone-fiber)) + ( up-pushout terminal-map terminal-map) + ( universal-property-suspension-fiber) + + equiv-fiber-codiagonal-map-suspension-fiber : + suspension (fiber f b) ≃ fiber (codiagonal-map f) b + pr1 equiv-fiber-codiagonal-map-suspension-fiber = + fiber-codiagonal-map-suspension-fiber + pr2 equiv-fiber-codiagonal-map-suspension-fiber = + is-equiv-fiber-codiagonal-map-suspension-fiber +``` From e4b0e89667ae08b0de37d09268ac7131fa4dd905 Mon Sep 17 00:00:00 2001 From: Tom de Jong <43781735+tomdjong@users.noreply.github.com> Date: Mon, 30 Oct 2023 15:29:57 +0000 Subject: [PATCH 2/3] The acyclic maps are exactly the epimorphisms (#894) --- .../acyclic-maps.lagda.md | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index a19d58f7d3..dd2ae13ff5 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -7,11 +7,17 @@ module synthetic-homotopy-theory.acyclic-maps where
Imports ```agda +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.epimorphisms +open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.propositions open import foundation.universe-levels open import synthetic-homotopy-theory.acyclic-types +open import synthetic-homotopy-theory.codiagonals-of-maps +open import synthetic-homotopy-theory.suspensions-of-types ```
@@ -41,6 +47,35 @@ module _ is-prop-is-acyclic-map f = is-prop-type-Prop (is-acyclic-map-Prop f) ``` +## Properties + +### A map is acyclic if and only if it is an [epimorphism](foundation.epimorphisms.md) + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-acyclic-map-is-epimorphism : is-epimorphism f → is-acyclic-map f + is-acyclic-map-is-epimorphism e b = + is-contr-equiv + ( fiber (codiagonal-map f) b) + ( equiv-fiber-codiagonal-map-suspension-fiber f b) + ( is-contr-map-is-equiv + ( is-equiv-codiagonal-map-is-epimorphism f e) + ( b)) + + is-epimorphism-is-acyclic-map : is-acyclic-map f → is-epimorphism f + is-epimorphism-is-acyclic-map ac = + is-epimorphism-is-equiv-codiagonal-map f + ( is-equiv-is-contr-map + ( λ b → + is-contr-equiv + ( suspension (fiber f b)) + ( inv-equiv (equiv-fiber-codiagonal-map-suspension-fiber f b)) + ( ac b))) +``` + ## See also - [Dependent epimorphisms](foundation.dependent-epimorphisms.md) From 0ea91d68392b1cabaad0e5b5a712cdfab687a4c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Mon, 30 Oct 2023 20:04:49 +0100 Subject: [PATCH 3/3] Equivalence between spans and relations (#889) --- src/foundation/spans.lagda.md | 69 ++++++++++++++++++- ...sal-property-dependent-pair-types.lagda.md | 4 ++ 2 files changed, 70 insertions(+), 3 deletions(-) diff --git a/src/foundation/spans.lagda.md b/src/foundation/spans.lagda.md index 7b85d5b6d9..da709f7fb7 100644 --- a/src/foundation/spans.lagda.md +++ b/src/foundation/spans.lagda.md @@ -8,16 +8,22 @@ module foundation.spans where ```agda open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.structure-identity-principle +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.type-duality +open import foundation.type-theoretic-principle-of-choice open import foundation.univalence +open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.commuting-triangles-of-maps open import foundation-core.contractible-types -open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types @@ -135,8 +141,65 @@ module _ ### Spans are equivalent to binary relations -This remains to be shown. -[#767](https://github.com/UniMath/agda-unimath/issues/767) +Using the principles of [type duality](foundation.type-duality.md) and +[type theoretic principle of choice](foundation.type-theoretic-principle-of-choice.md), +we can show that the type of spans `A <-- S --> B` is +[equivalent](foundation.equivalences.md) to the type of type-valued binary +relations `A → B → 𝓤`. + +```agda +module _ + { l1 l2 l : Level} (A : UU l1) (B : UU l2) + where + + equiv-span-binary-relation : + ( A → B → UU (l1 ⊔ l2 ⊔ l)) ≃ span (l1 ⊔ l2 ⊔ l) A B + equiv-span-binary-relation = + ( associative-Σ (UU (l1 ⊔ l2 ⊔ l)) (λ X → X → A) (λ T → pr1 T → B)) ∘e + ( equiv-Σ (λ T → pr1 T → B) (equiv-Pr1 (l2 ⊔ l) A) (λ P → equiv-ind-Σ)) ∘e + ( distributive-Π-Σ) ∘e + ( equiv-Π-equiv-family + ( λ a → equiv-Pr1 (l1 ⊔ l) B)) + + span-binary-relation : + ( A → B → UU (l1 ⊔ l2 ⊔ l)) → span (l1 ⊔ l2 ⊔ l) A B + pr1 (span-binary-relation R) = Σ A (λ a → Σ B (λ b → R a b)) + pr1 (pr2 (span-binary-relation R)) = pr1 + pr2 (pr2 (span-binary-relation R)) = pr1 ∘ pr2 + + compute-span-binary-relation : + map-equiv equiv-span-binary-relation ~ span-binary-relation + compute-span-binary-relation = refl-htpy + + binary-relation-span : + span (l1 ⊔ l2 ⊔ l) A B → (A → B → UU (l1 ⊔ l2 ⊔ l)) + binary-relation-span S a b = + Σ ( domain-span S) + ( λ s → (left-map-span S s ＝ a) × (right-map-span S s ＝ b)) + + compute-binary-relation-span : + map-inv-equiv equiv-span-binary-relation ~ binary-relation-span + compute-binary-relation-span S = + inv + ( map-eq-transpose-equiv equiv-span-binary-relation + ( eq-htpy-span + ( l1 ⊔ l2 ⊔ l) + ( A) + ( B) + ( _) + ( _) + ( ( equiv-pr1 (λ s → is-torsorial-path (left-map-span S s))) ∘e + ( equiv-left-swap-Σ) ∘e + ( equiv-tot + ( λ a → + ( equiv-tot + ( λ s → + equiv-pr1 (λ _ → is-torsorial-path (right-map-span S s)) ∘e + equiv-left-swap-Σ)) ∘e + ( equiv-left-swap-Σ))) , + ( inv-htpy (pr1 ∘ pr2 ∘ pr2 ∘ pr2)) , + ( inv-htpy (pr2 ∘ pr2 ∘ pr2 ∘ pr2))))) +``` ## See also diff --git a/src/foundation/universal-property-dependent-pair-types.lagda.md b/src/foundation/universal-property-dependent-pair-types.lagda.md index 1ceba44e79..b3a81fd5ef 100644 --- a/src/foundation/universal-property-dependent-pair-types.lagda.md +++ b/src/foundation/universal-property-dependent-pair-types.lagda.md @@ -44,6 +44,10 @@ module _ equiv-ev-pair : ((x : Σ A B) → C x) ≃ ((a : A) (b : B a) → C (pair a b)) pr1 equiv-ev-pair = ev-pair pr2 equiv-ev-pair = is-equiv-ev-pair + + equiv-ind-Σ : ((a : A) (b : B a) → C (a , b)) ≃ ((x : Σ A B) → C x) + pr1 equiv-ind-Σ = ind-Σ + pr2 equiv-ind-Σ = is-equiv-ind-Σ ``` ## Properties