Span diagrams (#1007)

This pull request contains the changes from #885 that don't touch
`synthetic-homotopy-theory` or `structured-types`, except those changes
that are necessary to make the library compile.

This PR contains the following changes:
- Disambigating between spans and span diagrams. The disambiguation is
explained in the relevant files.
- Developing infrastructure for spans and span diagrams, with the goal
of making it useful for pushouts.
- Add extensive informal explanations to all the new files and to
relevant existing files.
- Change `is-injective-map-equiv` to `is-injective-equiv`, because I
needed the fact that `map-equiv` is an injective map somewhere.
- Refactors binary type duality and generalises the handling of
universes for some of the components of binary type duality. We note
specifically by avoiding a proof by equivalence reasoning, it was a lot
easier to get the underlying equivalences to do the expected thing.
Proofs by equivalence reasoning are more suitable in proofs where the
actual equivalence is of less importance, such as `abstract` proofs.
- A note on equivalence reasoning was added to
`foundation-core.equivalences.lagda.md` to record the previous point on
the website.
- During the development of #885 I have left a lot of `{{#concept }}`
macros with unattributed `Agda` fields. The quickest way to clean that
up was just to run through all places where the macro was used and see
if there are any unattributed fields. So I did that throughout the
library. This includes for files that I would otherwise not have
touched, because it didn't make sense to break up my workflow just for
them.

Thanks for @VojtechStep for the idea of breaking down #885 into smaller
pull requests.

src/elementary-number-theory/cubes-natural-numbers.lagda.md

@@ -20,7 +20,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-The {{#concept "cube" Disambiguation="natural number"}} `n³` of a
+The {{#concept "cube" Disambiguation="natural number" Agda=cube-ℕ}} `n³` of a
 [natural number](elementary-number-theory.natural-numbers.md) `n` is the triple
 [product](elementary-number-theory.multiplication-natural-numbers.md)
 

src/elementary-number-theory/multiplication-natural-numbers.lagda.md

@@ -25,9 +25,9 @@ open import foundation.negated-equality
 
 ## Idea
 
-The {{#concept "multiplication" Disambiguation="natural numbers"}} operation on
-the [natural numbers](elementary-number-theory.natural-numbers.md) is defined by
-[iteratively](foundation.iterating-functions.md) applying
+The {{#concept "multiplication" Disambiguation="natural numbers" Agda=mul-ℕ}}
+operation on the [natural numbers](elementary-number-theory.natural-numbers.md)
+is defined by [iteratively](foundation.iterating-functions.md) applying
 [addition](elementary-number-theory.addition-natural-numbers.md) of a number to
 itself. More preciesly the number `m * n` is defined by adding the number `n` to
 itself `m` times:

src/elementary-number-theory/squares-natural-numbers.lagda.md

@@ -30,8 +30,8 @@ open import foundation-core.transport-along-identifications
 
 ## Idea
 
-The {{#concept "square" Disambiguation="natural number"}} `n²` of a
-[natural number](elementary-number-theory.natural-numbers.md) `n` is the
+The {{#concept "square" Disambiguation="natural number" Agda=square-ℕ}} `n²` of
+a [natural number](elementary-number-theory.natural-numbers.md) `n` is the
 [product](elementary-number-theory.multiplication-natural-numbers.md)
 
 ```text

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -614,7 +614,7 @@ module _
               ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))))
             ( this-third-thing n p)
             ( map-quotient-loop-Fin n p (this-third-thing n p)))
-          ( is-injective-map-equiv (inv-equiv (that-thing n)) (q ∙ inv r))))
+          ( is-injective-equiv (inv-equiv (that-thing n)) (q ∙ inv r))))
   cases-eq-map-quotient-aut-Fin n p (inr ND) (inl (inr star)) (inr star) q r =
     ( ap
       ( map-equiv (that-thing n))
@@ -650,7 +650,7 @@ module _
               ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))))
             ( this-third-thing n p)
             ( map-quotient-loop-Fin n p (this-third-thing n p)))
-          ( is-injective-map-equiv (inv-equiv (that-thing n)) (q ∙ inv r))))
+          ( is-injective-equiv (inv-equiv (that-thing n)) (q ∙ inv r))))
 
   eq-map-quotient-aut-Fin :
     (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) →

src/finite-group-theory/orbits-permutations.lagda.md

@@ -281,7 +281,7 @@ module _
                   ( λ x → le-ℕ x first-point-min-repeating)
                   ( equality-pred-second)
                   ( le-min-reporting)))
-              ( is-injective-map-equiv
+              ( is-injective-equiv
                 ( f)
                 ( tr
                   ( λ x →
@@ -1900,7 +1900,7 @@ module _
           ( inl k)
       section-h'-inl k (inl Q) R (inl Q') R' =
         ap inl
-          ( is-injective-map-equiv (equiv-count h)
+          ( is-injective-equiv (equiv-count h)
             ( ap
               ( λ f → map-equiv f (class (same-orbits-permutation-count g) a))
               ( right-inverse-law-equiv (equiv-count h)) ∙

src/finite-group-theory/permutations-standard-finite-types.lagda.md

@@ -213,7 +213,7 @@ abstract
         ( neq-inr-inl)
         ( λ r →
           neq-inr-inl
-            ( is-injective-map-equiv f (p ∙ (r ∙ inv q))))
+            ( is-injective-equiv f (p ∙ (r ∙ inv q))))
     lemma :
       Id
         ( map-equiv
@@ -404,7 +404,7 @@ abstract
     (succ-ℕ n) f (inr star) p (inl y) (inr star) q =
     ex-falso
       ( neq-inr-inl
-        ( is-injective-map-equiv f (p ∙ inv q)))
+        ( is-injective-equiv f (p ∙ inv q)))
   retraction-permutation-list-transpositions-Fin'
     (succ-ℕ n) f (inr star) p (inr star) z q =
     ap

src/finite-group-theory/transpositions.lagda.md

@@ -403,29 +403,29 @@ module _
       ( Id (pr1 two-elements-transposition) x) +
       ( Id (pr1 (pr2 two-elements-transposition)) x)
     cases-coprod-id-type-t x p h (inl (inr star)) (inl (inr star)) k3 K1 K2 K3 =
-      inl (ap pr1 (is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K1)))
+      inl (ap pr1 (is-injective-equiv (inv-equiv h) (K2 ∙ inv K1)))
     cases-coprod-id-type-t x p h
       (inl (inr star)) (inr star) (inl (inr star)) K1 K2 K3 =
-      inr (ap pr1 (is-injective-map-equiv (inv-equiv h) (K3 ∙ inv K1)))
+      inr (ap pr1 (is-injective-equiv (inv-equiv h) (K3 ∙ inv K1)))
     cases-coprod-id-type-t x p h
       (inl (inr star)) (inr star) (inr star) K1 K2 K3 =
       ex-falso
         ( pr2 element-is-not-identity-map-transposition
         ( inv
           ( ap pr1
-            ( is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K3)))))
+            ( is-injective-equiv (inv-equiv h) (K2 ∙ inv K3)))))
     cases-coprod-id-type-t x p h
       (inr star) (inl (inr star)) (inl (inr star)) K1 K2 K3 =
       ex-falso
         ( pr2 element-is-not-identity-map-transposition
         ( inv
           ( ap pr1
-            ( is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K3)))))
+            ( is-injective-equiv (inv-equiv h) (K2 ∙ inv K3)))))
     cases-coprod-id-type-t x p h
       (inr star) (inl (inr star)) (inr star) K1 K2 K3 =
-      inr (ap pr1 (is-injective-map-equiv (inv-equiv h) (K3 ∙ inv K1)))
+      inr (ap pr1 (is-injective-equiv (inv-equiv h) (K3 ∙ inv K1)))
     cases-coprod-id-type-t x p h (inr star) (inr star) k3 K1 K2 K3 =
-      inl (ap pr1 (is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K1)))
+      inl (ap pr1 (is-injective-equiv (inv-equiv h) (K2 ∙ inv K1)))
     coprod-id-type-t :
       (x : X) → type-Decidable-Prop (pr1 Y x) →
       ( Id (pr1 two-elements-transposition) x) +
@@ -673,7 +673,7 @@ module _
   pr1 (pr2 (pr1 (transposition-conjugation-equiv (pair P H)) x)) =
     is-prop-all-elements-equal
       (λ p1 p2 →
-        is-injective-map-equiv
+        is-injective-equiv
           ( inv-equiv
             ( compute-raise l4 (type-Decidable-Prop (P (map-inv-equiv e x)))))
           ( eq-is-prop (is-prop-type-Decidable-Prop (P (map-inv-equiv e x)))))
@@ -781,7 +781,7 @@ module _
                 ( pair (Σ X (λ y → type-Decidable-Prop (pr1 t y))) (pr2 t))
                 { pair (map-inv-equiv e x) p}
                 ( eq-pair-Σ
-                  ( is-injective-map-equiv
+                  ( is-injective-equiv
                     ( e)
                     ( inv (pr1 (pair-eq-Σ q)) ∙
                       ap
@@ -1013,13 +1013,13 @@ eq-transposition-precomp-standard-2-Element-Decidable-Subtype
     pr1 (pr1 (standard-2-Element-Decidable-Subtype H np) z)
   f z (inl p) =
     inr
-      ( is-injective-map-equiv
+      ( is-injective-equiv
         ( standard-transposition H np)
         ( ( right-computation-standard-transposition H np) ∙
           ( p)))
   f z (inr p) =
     inl
-      ( is-injective-map-equiv
+      ( is-injective-equiv
         ( standard-transposition H np)
         ( ( left-computation-standard-transposition H np) ∙
           ( p)))
@@ -1087,13 +1087,13 @@ eq-transposition-precomp-ineq-standard-2-Element-Decidable-Subtype
     pr1 (pr1 (standard-2-Element-Decidable-Subtype H np') u)
   f u (inl p) =
     inl
-      ( is-injective-map-equiv
+      ( is-injective-equiv
         ( standard-transposition H np)
         ( ( is-fixed-point-standard-transposition H np z nq1 nq3) ∙
           ( p)))
   f u (inr p) =
     inr
-      ( is-injective-map-equiv
+      ( is-injective-equiv
         ( standard-transposition H np)
         ( ( is-fixed-point-standard-transposition H np w nq2 nq4) ∙
           ( p)))

src/foundation-core.lagda.md

@@ -36,6 +36,8 @@ open import foundation-core.identity-types public
 open import foundation-core.injective-maps public
 open import foundation-core.invertible-maps public
 open import foundation-core.negation public
+open import foundation-core.operations-span-diagrams public
+open import foundation-core.operations-spans public
 open import foundation-core.path-split-maps public
 open import foundation-core.postcomposition-functions public
 open import foundation-core.precomposition-dependent-functions public

src/foundation-core/commuting-squares-of-maps.lagda.md

@@ -219,6 +219,6 @@ module _
 
 Several structures make essential use of commuting squares of maps:
 
-- [Cones over cospans](foundation.cones-over-cospans.md)
-- [Cocones under spans](synthetic-homotopy-theory.cocones-under-spans.md)
+- [Cones over cospan diagrams](foundation.cones-over-cospan-diagrams.md)
+- [Cocones under span diagrams](synthetic-homotopy-theory.cocones-under-spans.md)
 - [Morphisms of arrows](foundation.morphisms-arrows.md)

src/foundation-core/equivalences.lagda.md

@@ -714,6 +714,23 @@ equivalence-reasoning
 The equivalence constructed in this way is `equiv-1 ∘e (equiv-2 ∘e equiv-3)`,
 i.e., the equivivalence is associated fully to the right.
 
+**Note.** In situations where it is important to have precise control over an
+equivalence or its inverse, it is often better to avoid making use of
+equivalence reasoning. For example, since many of the entries proving that a map
+is an equivalence are marked as `abstract` in agda-unimath, the inverse of an
+equivalence often does not compute to any map that one might expect the inverse
+to be. If inverses of equivalences are used in equivalence reasoning, this
+results in a composed equivalence that also does not compute to any expected
+underlying map.
+
+Even if a proof by equivalence reasoning is clear to the human reader,
+constructing equivalences by hand by constructing maps back and forth and two
+homotopies witnessing that they are mutual inverses is often the most
+straigtforward solution that gives the best expected computational behavior of
+the constructed equivalence. In particular, if the underlying map or its inverse
+are noteworthy maps, it is good practice to define them directly rather than as
+underlying maps of equivalences constructed by equivalence reasoning.
+
 ```agda
 infixl 1 equivalence-reasoning_
 infixl 0 step-equivalence-reasoning

src/foundation-core/functoriality-dependent-function-types.lagda.md

@@ -121,7 +121,7 @@ module _
     ( map-inv-equiv (equiv-Π-equiv-family e)) ~
     ( map-equiv (equiv-Π-equiv-family (λ x → inv-equiv (e x))))
   compute-inv-equiv-Π-equiv-family e f =
-    is-injective-map-equiv
+    is-injective-equiv
       ( equiv-Π-equiv-family e)
       ( ( is-section-map-inv-equiv (equiv-Π-equiv-family e) f) ∙
         ( eq-htpy (λ x → inv (is-section-map-inv-equiv (e x) (f x)))))

src/foundation-core/injective-maps.lagda.md

@@ -114,8 +114,8 @@ module _
         ( is-retraction-map-inv-is-equiv H y))
 
   abstract
-    is-injective-map-equiv : (e : A ≃ B) → is-injective (map-equiv e)
-    is-injective-map-equiv (pair f H) = is-injective-is-equiv H
+    is-injective-equiv : (e : A ≃ B) → is-injective (map-equiv e)
+    is-injective-equiv (pair f H) = is-injective-is-equiv H
 
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}