Pullbacks of synthetic categories (#1183)

This PR contains the axioms for pullbacks of synthetic categories
together with the needed infrastructure, such as cospans and cone
diagrams.
It seemed impossible to do this with the existing axioms, so I
postulated an additional axiom which states that given natural
isomorphisms α β γ δ (with appropriate domains and codomains) together
with 3-isomorphisms α≅γ and β≅δ, there is an isomorphism of respective
horizontal composites: β * α≅δ * γ. I suppose this axiom is validatd by
Makkai's principle.
Note also that some lines exceed the maximum character limit. I wasn't
sure how to avoid this since I tried to avoid ad-hoc renamings and `let`
statement.

src/synthetic-category-theory.lagda.md

@@ -25,7 +25,13 @@ Some core principles of higher category theory include:
 ```agda
 module synthetic-category-theory where
 
-open import synthetic-category-theory.equivalence-of-synthetic-categories public
+open import synthetic-category-theory.cone-diagrams-synthetic-categories public
+open import synthetic-category-theory.cospans-synthetic-categories public
+open import synthetic-category-theory.equivalences-synthetic-categories public
+open import synthetic-category-theory.invertible-functors-synthetic-categories public
+open import synthetic-category-theory.pullbacks-synthetic-categories public
+open import synthetic-category-theory.retractions-synthetic-categories public
+open import synthetic-category-theory.sections-synthetic-categories public
 open import synthetic-category-theory.synthetic-categories public
 ```
 

src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md

@@ -0,0 +1,168 @@
+# Equivalences between synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.equivalences-synthetic-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import structured-types.globular-types
+
+open import synthetic-category-theory.retractions-synthetic-categories
+open import synthetic-category-theory.sections-synthetic-categories
+open import synthetic-category-theory.synthetic-categories
+```
+
+</details>
+
+## Idea
+
+A functor f: A → B of
+[synthetic categories](synthetic-category-theory.synthetic-categories.md) is an
+{{#concept "equivalence" Disambiguation="Synthetic categories}} if it has a
+[section](synthetic-category-theory.sections-synthetic-categories.md) and a
+[retraction](synthetic-category-theory.retractions-synthetic-categories.md).
+
+### The predicate of being an equivalence
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (f : functor-Synthetic-Category-Theory κ C D) → UU l
+  is-equiv-Synthetic-Category-Theory κ μ ι f =
+    ( section-Synthetic-Category-Theory κ μ ι f)
+      ×
+    ( retraction-Synthetic-Category-Theory κ μ ι f)
+```
+
+### The components of a proof of being an equivalence
+
+```agda
+module _
+  {l : Level}
+  where
+
+  section-is-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ}
+    {f : functor-Synthetic-Category-Theory κ C D} →
+    is-equiv-Synthetic-Category-Theory κ μ ι f →
+    section-Synthetic-Category-Theory κ μ ι f
+  section-is-equiv-Synthetic-Category-Theory κ μ ι = pr1
+
+  retraction-is-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ}
+    {f : functor-Synthetic-Category-Theory κ C D} →
+    is-equiv-Synthetic-Category-Theory κ μ ι f →
+    retraction-Synthetic-Category-Theory κ μ ι f
+  retraction-is-equiv-Synthetic-Category-Theory κ μ ι = pr2
+```
+
+### The type of equivalences between two given synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (C D : category-Synthetic-Category-Theory κ) → UU l
+  equiv-Synthetic-Category-Theory κ μ ι C D =
+    Σ ( functor-Synthetic-Category-Theory κ C D)
+      ( is-equiv-Synthetic-Category-Theory κ μ ι)
+```
+
+### The components of an equivalence of synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  functor-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ) →
+    equiv-Synthetic-Category-Theory κ μ ι C D →
+    functor-Synthetic-Category-Theory κ C D
+  functor-equiv-Synthetic-Category-Theory κ μ ι = pr1
+
+  is-equiv-functor-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ) →
+    (H : equiv-Synthetic-Category-Theory κ μ ι C D) →
+    is-equiv-Synthetic-Category-Theory κ μ ι
+      ( functor-equiv-Synthetic-Category-Theory κ μ ι H)
+  is-equiv-functor-equiv-Synthetic-Category-Theory κ μ ι = pr2
+
+  section-functor-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ}
+    (H : equiv-Synthetic-Category-Theory κ μ ι C D) →
+    section-Synthetic-Category-Theory κ μ ι
+      ( functor-equiv-Synthetic-Category-Theory κ μ ι H)
+  section-functor-equiv-Synthetic-Category-Theory κ μ ι H =
+    section-is-equiv-Synthetic-Category-Theory κ μ ι
+      ( is-equiv-functor-equiv-Synthetic-Category-Theory κ μ ι H)
+
+  functor-section-functor-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ}
+    (H : equiv-Synthetic-Category-Theory κ μ ι C D) →
+    functor-Synthetic-Category-Theory κ D C
+  functor-section-functor-equiv-Synthetic-Category-Theory κ μ ι H =
+    functor-section-Synthetic-Category-Theory κ μ ι
+      ( section-functor-equiv-Synthetic-Category-Theory κ μ ι H)
+
+  retraction-functor-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ}
+    (H : equiv-Synthetic-Category-Theory κ μ ι C D) →
+    retraction-Synthetic-Category-Theory κ μ ι
+      ( functor-equiv-Synthetic-Category-Theory κ μ ι H)
+  retraction-functor-equiv-Synthetic-Category-Theory κ μ ι H =
+    retraction-is-equiv-Synthetic-Category-Theory κ μ ι
+      ( is-equiv-functor-equiv-Synthetic-Category-Theory κ μ ι H)
+
+  functor-retraction-functor-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ}
+    (H : equiv-Synthetic-Category-Theory κ μ ι C D) →
+    functor-Synthetic-Category-Theory κ D C
+  functor-retraction-functor-equiv-Synthetic-Category-Theory κ μ ι H =
+    functor-retraction-Synthetic-Category-Theory κ μ ι
+      ( retraction-functor-equiv-Synthetic-Category-Theory κ μ ι H)
+```