Merge branch 'master' into pct

CONTRIBUTORS.toml

@@ -54,6 +54,18 @@ implementing the functional programming language Juvix. His PhD research is on
 graph theory from a univalent point of view.
 '''
 
+[[contributors]]
+displayName = "Vojtěch Štěpančík"
+maintainer = true
+usernames = [ "Vojtěch Štěpančík", "VojtechStep" ]
+homepage = "https://vojtechstep.eu/"
+github = "VojtechStep"
+bio = '''
+Vojtěch is a master\'s student at Charles University in Prague. His background
+is in software engineering, and he\'s working on formalizing synthetic
+homotopy theoretic topics for his thesis.
+'''
+
 [[contributors]]
 displayName = "Eléonore Mangel"
 usernames = [ "Eléonore Mangel", "EleonoreMangel", "Léo Mangel", "LeoMangel" ]
@@ -79,12 +91,6 @@ displayName = "Victor Blanchi"
 usernames = [ "VictorBlanchi" ]
 github = "VictorBlanchi"
 
-[[contributors]]
-displayName = "Vojtěch Štěpančík"
-usernames = [ "Vojtěch Štěpančík", "VojtechStep" ]
-homepage = "https://vojtechstep.eu/"
-github = "VojtechStep"
-
 [[contributors]]
 displayName = "Fernando Chu"
 usernames = [ "Fernando Chu", "fernando" ]

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -105,6 +105,14 @@ module _
 
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
   η-pair t = eq-pair-Σ refl refl
+
+  eq-base-eq-pair : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
+  eq-base-eq-pair p = pr1 (pair-eq-Σ p)
+
+  dependent-eq-family-eq-pair :
+    {s t : Σ A B} → (p : s ＝ t) →
+    dependent-identification B (eq-base-eq-pair p) (pr2 s) (pr2 t)
+  dependent-eq-family-eq-pair p = pr2 (pair-eq-Σ p)
 ```
 
 ### Lifting equality to the total space

src/foundation/homotopies.lagda.md

@@ -20,6 +20,7 @@ open import foundation.identity-types
 open import foundation.path-algebra
 open import foundation.universe-levels
 
+open import foundation-core.dependent-identifications
 open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-function-types
@@ -208,12 +209,19 @@ module _
 
   compute-dependent-identification-eq-value :
     {x y : A} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
-    (((apd f p) ∙ r) ＝ ((ap (tr B p) q) ∙ (apd g p))) ≃
-    (tr (eq-value f g) p q ＝ r)
+    coherence-square-identifications (ap (tr B p) q) (apd f p) (apd g p) r ≃
+    dependent-identification (eq-value f g) p q r
   pr1 (compute-dependent-identification-eq-value p q r) =
     map-compute-dependent-identification-eq-value f g p q r
   pr2 (compute-dependent-identification-eq-value p q r) =
     is-equiv-map-compute-dependent-identification-eq-value p q r
+
+  inv-map-compute-dependent-identification-eq-value :
+    {x y : A} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
+    dependent-identification (eq-value f g) p q r →
+    coherence-square-identifications (ap (tr B p) q) (apd f p) (apd g p) r
+  inv-map-compute-dependent-identification-eq-value p q r =
+    map-inv-equiv (compute-dependent-identification-eq-value p q r)
 ```
 
 ### Computing dependent-identifications in the type family `eq-value` of ordinary functions
@@ -224,23 +232,30 @@ module _
   where
 
   is-equiv-map-compute-dependent-identification-eq-value-function :
-    {x y : A} (p : x ＝ y) (q : eq-value f g x) (q' : eq-value f g y) →
-    is-equiv (map-compute-dependent-identification-eq-value-function f g p q q')
-  is-equiv-map-compute-dependent-identification-eq-value-function refl q q' =
+    {x y : A} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
+    is-equiv (map-compute-dependent-identification-eq-value-function f g p q r)
+  is-equiv-map-compute-dependent-identification-eq-value-function refl q r =
     is-equiv-comp
       ( inv)
-      ( concat' q' right-unit)
-      ( is-equiv-concat' q' right-unit)
-      ( is-equiv-inv q' q)
+      ( concat' r right-unit)
+      ( is-equiv-concat' r right-unit)
+      ( is-equiv-inv r q)
 
   compute-dependent-identification-eq-value-function :
-    {a0 a1 : A} (p : a0 ＝ a1) (q : f a0 ＝ g a0) (q' : f a1 ＝ g a1) →
-    ( coherence-square-identifications q (ap f p) (ap g p) q') ≃
-    ( tr (eq-value f g) p q ＝ q')
-  pr1 (compute-dependent-identification-eq-value-function p q q') =
-    map-compute-dependent-identification-eq-value-function f g p q q'
-  pr2 (compute-dependent-identification-eq-value-function p q q') =
-    is-equiv-map-compute-dependent-identification-eq-value-function p q q'
+    {x y : A} (p : x ＝ y) (q : f x ＝ g x) (r : f y ＝ g y) →
+    coherence-square-identifications q (ap f p) (ap g p) r ≃
+    dependent-identification (eq-value f g) p q r
+  pr1 (compute-dependent-identification-eq-value-function p q r) =
+    map-compute-dependent-identification-eq-value-function f g p q r
+  pr2 (compute-dependent-identification-eq-value-function p q r) =
+    is-equiv-map-compute-dependent-identification-eq-value-function p q r
+
+  inv-map-compute-dependent-identification-eq-value-function :
+    {x y : A} (p : x ＝ y) (q : f x ＝ g x) (r : f y ＝ g y) →
+    dependent-identification (eq-value f g) p q r →
+    coherence-square-identifications q (ap f p) (ap g p) r
+  inv-map-compute-dependent-identification-eq-value-function p q r =
+    map-inv-equiv (compute-dependent-identification-eq-value-function p q r)
 ```
 
 ### Relation between between `compute-dependent-identification-eq-value-function` and `nat-htpy`

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/structured-types/commuting-squares-of-pointed-maps.lagda.md

@@ -7,6 +7,8 @@ module structured-types.commuting-squares-of-pointed-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.function-types
 open import foundation.universe-levels
 
 open import structured-types.pointed-homotopies
@@ -35,12 +37,24 @@ between the pointedness preservation proofs.
 ## Definition
 
 ```agda
-coherence-square-pointed-maps :
+module _
   {l1 l2 l3 l4 : Level}
   {A : Pointed-Type l1} {B : Pointed-Type l2}
   {C : Pointed-Type l3} {X : Pointed-Type l4}
-  (top : C →∗ B) (left : C →∗ A) (right : B →∗ X) (bottom : A →∗ X) →
-  UU (l3 ⊔ l4)
-coherence-square-pointed-maps top left right bottom =
-  (bottom ∘∗ left) ~∗ (right ∘∗ top)
+  (top : C →∗ B) (left : C →∗ A) (right : B →∗ X) (bottom : A →∗ X)
+  where
+
+  coherence-square-pointed-maps : UU (l3 ⊔ l4)
+  coherence-square-pointed-maps =
+    bottom ∘∗ left ~∗ right ∘∗ top
+
+  coherence-square-maps-coherence-square-pointed-maps :
+    coherence-square-pointed-maps →
+    coherence-square-maps
+      ( map-pointed-map top)
+      ( map-pointed-map left)
+      ( map-pointed-map right)
+      ( map-pointed-map bottom)
+  coherence-square-maps-coherence-square-pointed-maps =
+    htpy-pointed-htpy (bottom ∘∗ left) (right ∘∗ top)
 ```

src/structured-types/pointed-homotopies.lagda.md

@@ -79,6 +79,8 @@ _~∗_ :
   pointed-Π A B → pointed-Π A B → UU (l1 ⊔ l2)
 _~∗_ {A = A} {B} = htpy-pointed-Π
 
+infix 6 _~∗_
+
 htpy-pointed-htpy :
   {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
   (f g : pointed-Π A B) → f ~∗ g →

src/structured-types/pointed-unit-type.lagda.md

@@ -12,6 +12,7 @@ open import foundation.identity-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import structured-types.pointed-homotopies
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
 ```
@@ -33,12 +34,26 @@ pr2 unit-Pointed-Type = star
 ## Properties
 
 ```agda
-terminal-pointed-map : {l : Level} (X : Pointed-Type l) → X →∗ unit-Pointed-Type
-pr1 (terminal-pointed-map X) _ = star
-pr2 (terminal-pointed-map X) = refl
-
-inclusion-point-Pointed-Type :
-  {l : Level} (X : Pointed-Type l) → unit-Pointed-Type →∗ X
-pr1 (inclusion-point-Pointed-Type X) = point (point-Pointed-Type X)
-pr2 (inclusion-point-Pointed-Type X) = refl
+module _
+  {l : Level} (X : Pointed-Type l)
+  where
+
+  terminal-pointed-map : X →∗ unit-Pointed-Type
+  pr1 terminal-pointed-map _ = star
+  pr2 terminal-pointed-map = refl
+
+  map-terminal-pointed-map : type-Pointed-Type X → unit
+  map-terminal-pointed-map =
+    map-pointed-map {A = X} {B = unit-Pointed-Type}
+      terminal-pointed-map
+
+  inclusion-point-Pointed-Type :
+    unit-Pointed-Type →∗ X
+  pr1 inclusion-point-Pointed-Type = point (point-Pointed-Type X)
+  pr2 inclusion-point-Pointed-Type = refl
+
+  is-initial-unit-Pointed-Type :
+    ( f : unit-Pointed-Type →∗ X) → f ~∗ inclusion-point-Pointed-Type
+  pr1 (is-initial-unit-Pointed-Type f) _ = preserves-point-pointed-map f
+  pr2 (is-initial-unit-Pointed-Type f) = inv right-unit
 ```

src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md

@@ -115,3 +115,42 @@ module _
     ( preserves-point-pointed-map
       ( horizontal-pointed-map-cocone-Pointed-Type f g c))
 ```
+
+### Computation with the cogap map for pointed types
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level}
+  {S : Pointed-Type l1} {A : Pointed-Type l2} {B : Pointed-Type l3}
+  ( f : S →∗ A) (g : S →∗ B)
+  { X : Pointed-Type l4} (c : type-cocone-Pointed-Type f g X)
+  where
+
+  compute-inl-cogap-Pointed-Type :
+    ( x : type-Pointed-Type A) →
+    ( map-cogap-Pointed-Type
+      ( f)
+      ( g)
+      ( c)
+      ( map-pointed-map (inl-pushout-Pointed-Type f g) x)) ＝
+    ( horizontal-map-cocone-Pointed-Type f g c x)
+  compute-inl-cogap-Pointed-Type =
+    compute-inl-cogap
+      ( map-pointed-map f)
+      ( map-pointed-map g)
+      ( cocone-type-cocone-Pointed-Type f g c)
+
+  compute-inr-cogap-Pointed-Type :
+    ( y : type-Pointed-Type B) →
+    ( map-cogap-Pointed-Type
+      ( f)
+      ( g)
+      ( c)
+      ( map-pointed-map (inr-pushout-Pointed-Type f g) y)) ＝
+    ( vertical-map-cocone-Pointed-Type f g c y)
+  compute-inr-cogap-Pointed-Type =
+    compute-inr-cogap
+      ( map-pointed-map f)
+      ( map-pointed-map g)
+      ( cocone-type-cocone-Pointed-Type f g c)
+```