Merge branch 'master' into universal-property-of-smash-products

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
 

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

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

@@ -7,11 +7,17 @@ module synthetic-homotopy-theory.acyclic-maps where
 <details><summary>Imports</summary>
 
 ```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
 ```
 
 </details>
@@ -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)

src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md

@@ -7,13 +7,23 @@ module synthetic-homotopy-theory.codiagonals-of-maps where
 <details><summary>Imports</summary>
 
 ```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
 ```
 
 </details>
@@ -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
+```