diff --git a/src/synthetic-category-theory.lagda.md b/src/synthetic-category-theory.lagda.md
index 9b8b60665e..5ff89a2169 100644
--- a/src/synthetic-category-theory.lagda.md
+++ b/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
 ```
 
diff --git a/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md b/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..b94a468b43
--- /dev/null
+++ b/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md
@@ -0,0 +1,596 @@
+# Cone diagrams of synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.cone-diagrams-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.cospans-synthetic-categories
+open import synthetic-category-theory.synthetic-categories
+```
+
+</details>
+
+## Idea
+
+Consider a [cospan](synthetic-category-theory.cospans-synthetic-categories.md) S
+= D --g--> E <--f-- C of
+[synthetic categories](synthetic-category-theory.synthetic-categories.md) and
+let T be a synthetic category. A
+{{#concept "cone diagram" Disambiguation="Synthetic categories}} over S with an
+apex T is a pair of functors p : T → C and r : T → D that assemble into a
+commutative square of the form:
+
+```text
+T --p--> C
+|        |
+r   τ⇙   f
+|        |
+v        v
+D --g--> E.
+```
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  where
+
+  cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (S : cospan-Synthetic-Category-Theory κ C D E)
+    (T : category-Synthetic-Category-Theory κ) → UU l
+  cone-diagram-Synthetic-Category-Theory κ μ S T =
+    Σ ( functor-Synthetic-Category-Theory
+        κ T (right-source-cospan-Synthetic-Category-Theory κ S))
+      ( λ tr →
+        Σ ( functor-Synthetic-Category-Theory
+            κ T (left-source-cospan-Synthetic-Category-Theory κ S))
+          ( λ tl →
+            isomorphism-Synthetic-Category-Theory κ
+              ( comp-functor-Synthetic-Category-Theory μ
+                ( right-functor-cospan-Synthetic-Category-Theory κ S) tr)
+              ( comp-functor-Synthetic-Category-Theory μ
+                ( left-functor-cospan-Synthetic-Category-Theory κ S) tl)))
+```
+
+### The components of a cospan of synthetic categories
+
+```agda
+  apex-cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ} →
+    cone-diagram-Synthetic-Category-Theory κ μ S T →
+    category-Synthetic-Category-Theory κ
+  apex-cone-diagram-Synthetic-Category-Theory κ μ {T = T} c = T
+
+  left-functor-cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    (c : cone-diagram-Synthetic-Category-Theory κ μ S T) →
+    functor-Synthetic-Category-Theory κ
+      ( apex-cone-diagram-Synthetic-Category-Theory κ μ c)
+      ( left-source-cospan-Synthetic-Category-Theory κ S)
+  left-functor-cone-diagram-Synthetic-Category-Theory κ μ c = pr1 (pr2 c)
+
+  right-functor-cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    (c : cone-diagram-Synthetic-Category-Theory κ μ S T) →
+    functor-Synthetic-Category-Theory κ
+      ( apex-cone-diagram-Synthetic-Category-Theory κ μ c)
+      ( right-source-cospan-Synthetic-Category-Theory κ S)
+  right-functor-cone-diagram-Synthetic-Category-Theory κ μ c = pr1 c
+
+  iso-cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    (c : cone-diagram-Synthetic-Category-Theory κ μ S T) →
+    isomorphism-Synthetic-Category-Theory κ
+      ( comp-functor-Synthetic-Category-Theory μ
+        ( right-functor-cospan-Synthetic-Category-Theory κ S)
+        ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+      ( comp-functor-Synthetic-Category-Theory μ
+        ( left-functor-cospan-Synthetic-Category-Theory κ S)
+        ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+  iso-cone-diagram-Synthetic-Category-Theory κ μ c = pr2 (pr2 c)
+```
+
+### Isomorphisms of cone diagrams
+
+An isomorphism between cone diagrams c = (tl, tr, τ) and c' = (tl', tr', τ') is
+a pair of natural isomorphisms φl : tl ≅ tl' and φr : tr ≅ tr' together with an
+isomorphism of natural isomorphisms H : τ ≅ τ'.
+
+```agda
+  iso-of-cone-diagrams-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ} →
+    cone-diagram-Synthetic-Category-Theory κ μ S T →
+    cone-diagram-Synthetic-Category-Theory κ μ S T → UU l
+  iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ {S = S} c c' =
+    Σ ( isomorphism-Synthetic-Category-Theory κ
+        ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+        ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c'))
+      ( λ φr →
+        Σ ( isomorphism-Synthetic-Category-Theory κ
+            ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c'))
+          ( λ φl →
+            commuting-square-isomorphisms-Synthetic-Category-Theory κ μ
+              ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+                ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                  ( id-iso-Synthetic-Category-Theory ι
+                    ( left-functor-cospan-Synthetic-Category-Theory κ S))
+                  ( φl))
+                ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                  ( id-iso-Synthetic-Category-Theory ι
+                    ( right-functor-cospan-Synthetic-Category-Theory κ S))
+                  ( φr))
+                ( iso-cone-diagram-Synthetic-Category-Theory κ μ c')))
+```
+
+### The components of an isomorphism of cone diagrams
+
+```agda
+  right-functor-iso-of-cone-diagrams-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    {c c' : cone-diagram-Synthetic-Category-Theory κ μ S T} →
+    (iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ c c') →
+    isomorphism-Synthetic-Category-Theory κ
+      ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+      ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c')
+  right-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+    κ μ ι Χ = pr1
+
+  left-functor-iso-of-cone-diagrams-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    {c c' : cone-diagram-Synthetic-Category-Theory κ μ S T} →
+    (iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ c c') →
+    isomorphism-Synthetic-Category-Theory κ
+      ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+      ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c')
+  left-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+    κ μ ι Χ ϕ = pr1 (pr2 ϕ)
+
+  isomorphism-iso-of-cone-diagrams-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    {c c' : cone-diagram-Synthetic-Category-Theory κ μ S T} →
+    (ϕ : iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ c c') →
+    commuting-square-isomorphisms-Synthetic-Category-Theory κ μ
+      ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( id-iso-Synthetic-Category-Theory ι
+            ( left-functor-cospan-Synthetic-Category-Theory κ S))
+          ( left-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+            κ μ ι Χ ϕ))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+        ( id-iso-Synthetic-Category-Theory ι
+          ( right-functor-cospan-Synthetic-Category-Theory κ S))
+        ( right-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+          κ μ ι Χ ϕ))
+      ( iso-cone-diagram-Synthetic-Category-Theory κ μ c')
+  isomorphism-iso-of-cone-diagrams-Synthetic-Category-Theory
+    κ μ ι Χ ϕ = pr2 (pr2 ϕ)
+```
+
+## Isomorphisms of isomorphisms of cone diagrams
+
+If ϕ = (φl, φr, H) and Ψ = (ψl, ψr, K) are two isomorphisms between cone
+diagrams c and c', an isomorphism between them is a pair of isomorphisms φl ≅ ψl
+and φr ≅ ψr under which H becomes isomorphic to K.
+
+```agda
+  iso-of-isos-of-cone-diagrams-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Μ :
+      preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+        κ ι μ Χ)
+    {S : cospan-Synthetic-Category-Theory κ C D E}
+    {T : category-Synthetic-Category-Theory κ}
+    {c c' : cone-diagram-Synthetic-Category-Theory κ μ S T}
+    (ϕ ψ : iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ c c') → UU l
+  iso-of-isos-of-cone-diagrams-Synthetic-Category-Theory
+    κ μ ι ν Χ Μ {S = S} {c = c} {c' = c'} ϕ ψ =
+    Σ ( isomorphism-Synthetic-Category-Theory
+        ( functor-globular-type-Synthetic-Category-Theory κ
+          ( _)
+          ( right-source-cospan-Synthetic-Category-Theory κ S))
+        ( right-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+          κ μ ι Χ ϕ)
+        ( right-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+          κ μ ι Χ ψ))
+      ( λ α →
+        Σ ( isomorphism-Synthetic-Category-Theory
+            ( functor-globular-type-Synthetic-Category-Theory κ
+              ( _)
+              ( left-source-cospan-Synthetic-Category-Theory κ S))
+            ( left-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+              κ μ ι Χ ϕ)
+            ( left-functor-iso-of-cone-diagrams-Synthetic-Category-Theory
+              κ μ ι Χ ψ))
+          ( λ β →
+            isomorphism-Synthetic-Category-Theory
+              ( functor-globular-type-Synthetic-Category-Theory
+                ( functor-globular-type-Synthetic-Category-Theory κ
+                  ( _)
+                  ( target-cospan-Synthetic-Category-Theory κ S))
+                ( comp-functor-Synthetic-Category-Theory μ
+                  ( right-functor-cospan-Synthetic-Category-Theory κ S)
+                  ( right-functor-cone-diagram-Synthetic-Category-Theory
+                    κ μ c))
+                ( comp-functor-Synthetic-Category-Theory μ
+                  ( left-functor-cospan-Synthetic-Category-Theory κ S)
+                  ( left-functor-cone-diagram-Synthetic-Category-Theory
+                    κ μ c')))
+              ( comp-iso-Synthetic-Category-Theory
+                ( composition-isomorphism-Synthetic-Category-Theory μ)
+                ( horizontal-comp-iso-Synthetic-Category-Theory
+                  ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                    Χ)
+                  ( id-iso-Synthetic-Category-Theory
+                    ( identity-isomorphism-Synthetic-Category-Theory ι)
+                    ( iso-cone-diagram-Synthetic-Category-Theory κ μ c'))
+                  ( preserves-isomorphism-horizontal-comp-iso-Synthetic-Category-Theory
+                    ( Μ)
+                    ( α)
+                    ( id-iso-Synthetic-Category-Theory
+                      ( identity-isomorphism-Synthetic-Category-Theory ι)
+                      ( id-iso-Synthetic-Category-Theory ι
+                        ( right-functor-cospan-Synthetic-Category-Theory
+                          κ S)))))
+                ( comp-iso-Synthetic-Category-Theory
+                  ( composition-isomorphism-Synthetic-Category-Theory μ)
+                  ( isomorphism-iso-of-cone-diagrams-Synthetic-Category-Theory
+                    κ μ ι Χ ϕ)
+                  ( horizontal-comp-iso-Synthetic-Category-Theory
+                    ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                      Χ)
+                    ( preserves-isomorphism-horizontal-comp-iso-Synthetic-Category-Theory
+                      ( Μ)
+                      ( inv-iso-Synthetic-Category-Theory
+                        ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                        ( β))
+                      ( id-iso-Synthetic-Category-Theory
+                        ( identity-isomorphism-Synthetic-Category-Theory ι)
+                        ( id-iso-Synthetic-Category-Theory ι
+                          ( left-functor-cospan-Synthetic-Category-Theory
+                            κ S))))
+                    ( id-iso-Synthetic-Category-Theory
+                      ( identity-isomorphism-Synthetic-Category-Theory ι)
+                      ( iso-cone-diagram-Synthetic-Category-Theory
+                        κ μ c)))))
+              ( isomorphism-iso-of-cone-diagrams-Synthetic-Category-Theory
+                κ μ ι Χ ψ)))
+```
+
+## Induced cones
+
+Given a cone c = (tl, tr, τ) over S with apex T and a functor s : R → T we
+construct an induced cone over S with apex R, defined as s*(c) = (tl∘s, tr∘s,
+τ*idₛ).
+
+```agda
+module _
+  {l : Level}
+  where
+
+  induced-cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    (S : cospan-Synthetic-Category-Theory κ C D E)
+    {T : category-Synthetic-Category-Theory κ}
+    (c : cone-diagram-Synthetic-Category-Theory κ μ S T)
+    {R : category-Synthetic-Category-Theory κ}
+    (s : functor-Synthetic-Category-Theory κ R T) →
+      cone-diagram-Synthetic-Category-Theory κ μ S R
+  induced-cone-diagram-Synthetic-Category-Theory κ μ ι ν Χ Α S c s =
+    comp-functor-Synthetic-Category-Theory μ
+      ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+      ( s) ,
+    comp-functor-Synthetic-Category-Theory μ
+      ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+      ( s) ,
+    comp-iso-Synthetic-Category-Theory μ
+      ( associative-comp-functor-Synthetic-Category-Theory Α
+        ( left-functor-cospan-Synthetic-Category-Theory κ S)
+        ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+        ( s))
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+          ( id-iso-Synthetic-Category-Theory ι s))
+        ( inv-iso-Synthetic-Category-Theory ν
+          ( associative-comp-functor-Synthetic-Category-Theory Α
+            ( right-functor-cospan-Synthetic-Category-Theory κ S)
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( s))))
+```
+
+## Induced isomorphisms of cone diagrams
+
+Given a cone over S with apex T and two functors s, t : R → T together with an
+isomorphism s ≅ t, we construct an isomorphism of cone diagrams between s*(c)
+and t*(c).
+
+```agda
+module _
+  {l : Level}
+  where
+
+  induced-iso-cone-diagram-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D E : category-Synthetic-Category-Theory κ}
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ξ :
+      preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+        κ μ Α Χ)
+    (I : interchange-composition-Synthetic-Category-Theory κ μ Χ)
+    (Μ :
+      preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+        κ ι μ Χ)
+    (N :
+      preserves-identity-horizontal-composition-Synthetic-Category-Theory
+        κ ι μ Χ)
+    (S : cospan-Synthetic-Category-Theory κ C D E)
+    {T : category-Synthetic-Category-Theory κ}
+    (c : cone-diagram-Synthetic-Category-Theory κ μ S T)
+    {R : category-Synthetic-Category-Theory κ}
+    (s t : functor-Synthetic-Category-Theory κ R T) →
+    isomorphism-Synthetic-Category-Theory κ s t →
+      iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ
+        ( induced-cone-diagram-Synthetic-Category-Theory κ μ ι ν Χ Α S c s)
+        ( induced-cone-diagram-Synthetic-Category-Theory κ μ ι ν Χ Α S c t)
+  induced-iso-cone-diagram-Synthetic-Category-Theory
+    κ μ ι ν Α Χ Λ Ρ Ξ I M N S c s t α =
+    horizontal-comp-iso-Synthetic-Category-Theory Χ
+      ( id-iso-Synthetic-Category-Theory ι
+        ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)) α ,
+    horizontal-comp-iso-Synthetic-Category-Theory Χ
+      ( id-iso-Synthetic-Category-Theory ι
+        ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)) α ,
+    pasting-commuting-squares-isomorphisms-Synthetic-Category-Theory κ μ ι ν Α Χ
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+          ( id-iso-Synthetic-Category-Theory ι
+            ( s)))
+        ( inv-iso-Synthetic-Category-Theory ν
+          ( associative-comp-functor-Synthetic-Category-Theory Α
+            ( right-functor-cospan-Synthetic-Category-Theory κ S)
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( s))))
+      ( associative-comp-functor-Synthetic-Category-Theory Α
+        ( left-functor-cospan-Synthetic-Category-Theory κ S)
+        ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+        ( s))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+        ( id-iso-Synthetic-Category-Theory ι
+          ( left-functor-cospan-Synthetic-Category-Theory κ S))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( id-iso-Synthetic-Category-Theory ι
+            ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+          ( α)))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+        ( id-iso-Synthetic-Category-Theory ι
+          ( right-functor-cospan-Synthetic-Category-Theory κ S))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( id-iso-Synthetic-Category-Theory ι
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+          ( α)))
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+          ( id-iso-Synthetic-Category-Theory ι t))
+        ( inv-iso-Synthetic-Category-Theory ν
+          ( associative-comp-functor-Synthetic-Category-Theory Α
+            ( right-functor-cospan-Synthetic-Category-Theory κ S)
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( t))))
+      ( associative-comp-functor-Synthetic-Category-Theory Α
+        ( left-functor-cospan-Synthetic-Category-Theory κ S)
+        ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+        ( t))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( id-iso-Synthetic-Category-Theory ι
+            (left-functor-cospan-Synthetic-Category-Theory κ S))
+          ( id-iso-Synthetic-Category-Theory ι
+            ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)))
+        ( α))
+      ( pasting-commuting-squares-isomorphisms-Synthetic-Category-Theory
+        κ μ ι ν Α Χ
+        ( inv-iso-Synthetic-Category-Theory ν
+          ( associative-comp-functor-Synthetic-Category-Theory Α
+            ( right-functor-cospan-Synthetic-Category-Theory κ S)
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( s)))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+          ( id-iso-Synthetic-Category-Theory ι s))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( id-iso-Synthetic-Category-Theory ι
+              ( left-functor-cospan-Synthetic-Category-Theory κ S))
+            ( id-iso-Synthetic-Category-Theory ι
+              ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c)))
+          ( α))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( id-iso-Synthetic-Category-Theory ι
+            ( right-functor-cospan-Synthetic-Category-Theory κ S))
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( id-iso-Synthetic-Category-Theory ι
+              ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+            ( α)))
+        ( inv-iso-Synthetic-Category-Theory ν
+          ( associative-comp-functor-Synthetic-Category-Theory Α
+            ( right-functor-cospan-Synthetic-Category-Theory κ S)
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( t)))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+          ( id-iso-Synthetic-Category-Theory ι t))
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( id-iso-Synthetic-Category-Theory ι
+              ( right-functor-cospan-Synthetic-Category-Theory κ S))
+            ( id-iso-Synthetic-Category-Theory ι
+              ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)))
+          ( α))
+        ( preserves-associativity-comp-functor-horizontal-comp-iso-inv-Synthetic-Category-Theory
+          κ μ ι ν Α Χ Λ Ρ Ξ
+          ( right-functor-cospan-Synthetic-Category-Theory κ S)
+          ( right-functor-cospan-Synthetic-Category-Theory κ S)
+          ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+          ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)
+          s t
+          ( id-iso-Synthetic-Category-Theory ι
+            ( right-functor-cospan-Synthetic-Category-Theory κ S))
+          ( id-iso-Synthetic-Category-Theory ι
+            ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+          ( α))
+        ( comp-iso-Synthetic-Category-Theory
+          ( composition-isomorphism-Synthetic-Category-Theory μ)
+          ( interchange-comp-functor-Synthetic-Category-Theory I
+            ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( id-iso-Synthetic-Category-Theory ι
+                ( right-functor-cospan-Synthetic-Category-Theory κ S))
+              ( id-iso-Synthetic-Category-Theory ι
+                ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ c)))
+            ( id-iso-Synthetic-Category-Theory ι t)
+            ( α))
+          ( comp-iso-Synthetic-Category-Theory
+            ( composition-isomorphism-Synthetic-Category-Theory μ)
+            ( preserves-isomorphism-horizontal-comp-iso-Synthetic-Category-Theory
+              ( M)
+              ( inv-iso-Synthetic-Category-Theory
+                ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                ( left-unit-law-comp-functor-Synthetic-Category-Theory
+                  ( left-unit-law-composition-isomorphism-Synthetic-Category-Theory
+                    Λ)
+                  ( α)))
+              ( comp-iso-Synthetic-Category-Theory
+                ( composition-isomorphism-Synthetic-Category-Theory μ)
+                ( horizontal-comp-iso-Synthetic-Category-Theory
+                  ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                    Χ)
+                  ( id-iso-Synthetic-Category-Theory
+                    ( identity-isomorphism-Synthetic-Category-Theory ι)
+                    ( iso-cone-diagram-Synthetic-Category-Theory κ μ c))
+                  ( inv-iso-Synthetic-Category-Theory
+                    ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                    ( preserves-identity-horizontal-comp-iso-Synthetic-Category-Theory
+                      N)))
+                ( inv-iso-Synthetic-Category-Theory
+                  ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                  ( right-unit-law-comp-functor-Synthetic-Category-Theory
+                    ( right-unit-law-composition-isomorphism-Synthetic-Category-Theory
+                      Ρ)
+                    ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)))))
+            ( comp-iso-Synthetic-Category-Theory
+              ( composition-isomorphism-Synthetic-Category-Theory μ)
+              ( preserves-isomorphism-horizontal-comp-iso-Synthetic-Category-Theory
+                ( M)
+                ( right-unit-law-comp-functor-Synthetic-Category-Theory
+                  ( right-unit-law-composition-isomorphism-Synthetic-Category-Theory
+                    Ρ)
+                  ( α))
+                ( comp-iso-Synthetic-Category-Theory
+                  ( composition-isomorphism-Synthetic-Category-Theory μ)
+                  ( left-unit-law-comp-functor-Synthetic-Category-Theory
+                    ( left-unit-law-composition-isomorphism-Synthetic-Category-Theory
+                      Λ)
+                    ( iso-cone-diagram-Synthetic-Category-Theory κ μ c))
+                  ( horizontal-comp-iso-Synthetic-Category-Theory
+                    ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                      Χ)
+                    ( preserves-identity-horizontal-comp-iso-Synthetic-Category-Theory
+                      N)
+                    ( id-iso-Synthetic-Category-Theory
+                      ( identity-isomorphism-Synthetic-Category-Theory ι)
+                      ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)))))
+                  ( inv-iso-Synthetic-Category-Theory
+                    ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                    ( interchange-comp-functor-Synthetic-Category-Theory I
+                      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                        ( id-iso-Synthetic-Category-Theory ι
+                          ( left-functor-cospan-Synthetic-Category-Theory κ S))
+                        ( id-iso-Synthetic-Category-Theory ι
+                          ( left-functor-cone-diagram-Synthetic-Category-Theory
+                            κ μ c)))
+                      ( iso-cone-diagram-Synthetic-Category-Theory κ μ c)
+                      ( α)
+                      ( id-iso-Synthetic-Category-Theory ι s)))))))
+      ( preserves-associativity-comp-functor-horizontal-comp-iso-Synthetic-Category-Theory
+        ( Ξ)
+        ( id-iso-Synthetic-Category-Theory ι
+          ( left-functor-cospan-Synthetic-Category-Theory κ S))
+        ( id-iso-Synthetic-Category-Theory ι
+          ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ c))
+        ( α))
+```
diff --git a/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md b/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..8051db1b1d
--- /dev/null
+++ b/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md
@@ -0,0 +1,411 @@
+# Cospans of synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.cospans-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.equivalences-synthetic-categories
+open import synthetic-category-theory.synthetic-categories
+```
+
+</details>
+
+## Idea
+
+A {{#concept "cospan" Disambiguation="Synthetic categories"}} of
+[synthetic categories](synthetic-category-theory.synthetic-categories.md) is a
+pair of functors f, g of synthetic categories with a common codomain:
+
+```text
+C --f--> E <--g-- D.
+```
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  where
+
+  cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (C E D : category-Synthetic-Category-Theory κ) → UU l
+  cospan-Synthetic-Category-Theory κ C E D =
+    Σ ( functor-Synthetic-Category-Theory κ C E)
+      ( λ f → functor-Synthetic-Category-Theory κ D E)
+```
+
+### The components of a cospan of synthetic categories
+
+```agda
+  left-source-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C E D : category-Synthetic-Category-Theory κ} →
+    cospan-Synthetic-Category-Theory κ C E D →
+    category-Synthetic-Category-Theory κ
+  left-source-cospan-Synthetic-Category-Theory κ {C = C} S = C
+
+  right-source-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C E D : category-Synthetic-Category-Theory κ} →
+    cospan-Synthetic-Category-Theory κ C E D →
+      category-Synthetic-Category-Theory κ
+  right-source-cospan-Synthetic-Category-Theory κ {D = D} S = D
+
+  target-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C E D : category-Synthetic-Category-Theory κ} →
+    cospan-Synthetic-Category-Theory κ C E D →
+    category-Synthetic-Category-Theory κ
+  target-cospan-Synthetic-Category-Theory κ {E = E} S = E
+
+  left-functor-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C E D : category-Synthetic-Category-Theory κ}
+    (S : cospan-Synthetic-Category-Theory κ C E D) →
+    functor-Synthetic-Category-Theory κ
+      ( left-source-cospan-Synthetic-Category-Theory κ S)
+      ( target-cospan-Synthetic-Category-Theory κ S)
+  left-functor-cospan-Synthetic-Category-Theory κ = pr1
+
+  right-functor-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C E D : category-Synthetic-Category-Theory κ}
+    (S : cospan-Synthetic-Category-Theory κ C E D) →
+    functor-Synthetic-Category-Theory κ
+      ( right-source-cospan-Synthetic-Category-Theory κ S)
+      ( target-cospan-Synthetic-Category-Theory κ S)
+  right-functor-cospan-Synthetic-Category-Theory κ = pr2
+```
+
+## Transformations of cospans of synthetic categories
+
+A transformation between cospans C --f--> E <--g-- D and C'--f'--> E' <--g'-- D'
+is commutative diagram of the form:
+
+```text
+C --f---> E <---g-- D
+|         |         |
+φ   τ⇙    χ    σ⇙   ψ
+|         |         |
+v         v         v
+C'--f'--> E' <--g'--D'.
+```
+
+```agda
+module _
+  {l : Level}
+  where
+
+  transformation-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    (S : cospan-Synthetic-Category-Theory κ C E D)
+    (S' : cospan-Synthetic-Category-Theory κ C' E' D') → UU l
+  transformation-cospan-Synthetic-Category-Theory κ μ S S' =
+    Σ ( functor-Synthetic-Category-Theory κ
+        ( left-source-cospan-Synthetic-Category-Theory κ S)
+        ( left-source-cospan-Synthetic-Category-Theory κ S'))
+      ( λ φ →
+        Σ ( functor-Synthetic-Category-Theory κ
+            ( target-cospan-Synthetic-Category-Theory κ S)
+            ( target-cospan-Synthetic-Category-Theory κ S'))
+          ( λ χ →
+            Σ ( functor-Synthetic-Category-Theory κ
+                ( right-source-cospan-Synthetic-Category-Theory κ S)
+                ( right-source-cospan-Synthetic-Category-Theory κ S'))
+              ( λ ψ →
+                Σ ( commuting-square-functors-Synthetic-Category-Theory κ μ
+                    ( left-functor-cospan-Synthetic-Category-Theory κ S)
+                    ( χ)
+                    ( φ)
+                    ( left-functor-cospan-Synthetic-Category-Theory κ S'))
+                  ( λ τ →
+                    commuting-square-functors-Synthetic-Category-Theory κ μ
+                      ( right-functor-cospan-Synthetic-Category-Theory κ S)
+                      ( χ)
+                      ( ψ)
+                      ( right-functor-cospan-Synthetic-Category-Theory κ S')))))
+```
+
+### The components of a transformation of cospans of synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  left-functor-transformation-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    transformation-cospan-Synthetic-Category-Theory κ μ S S' →
+    functor-Synthetic-Category-Theory κ
+      ( left-source-cospan-Synthetic-Category-Theory κ S)
+      ( left-source-cospan-Synthetic-Category-Theory κ S')
+  left-functor-transformation-cospan-Synthetic-Category-Theory κ μ H = pr1 H
+
+  right-functor-transformation-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    transformation-cospan-Synthetic-Category-Theory κ μ S S' →
+    functor-Synthetic-Category-Theory κ
+      ( right-source-cospan-Synthetic-Category-Theory κ S)
+      ( right-source-cospan-Synthetic-Category-Theory κ S')
+  right-functor-transformation-cospan-Synthetic-Category-Theory κ μ H =
+    pr1 (pr2 (pr2 H))
+
+  middle-functor-transformation-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    transformation-cospan-Synthetic-Category-Theory κ μ S S' →
+    functor-Synthetic-Category-Theory κ
+      ( target-cospan-Synthetic-Category-Theory κ S)
+      ( target-cospan-Synthetic-Category-Theory κ S')
+  middle-functor-transformation-cospan-Synthetic-Category-Theory κ μ H =
+    pr1 (pr2 H)
+
+  left-commuting-square-transformation-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'}
+    (H : transformation-cospan-Synthetic-Category-Theory κ μ S S') →
+    commuting-square-functors-Synthetic-Category-Theory κ μ
+      ( left-functor-cospan-Synthetic-Category-Theory κ S)
+      ( middle-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+      ( left-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+      ( left-functor-cospan-Synthetic-Category-Theory κ S')
+  left-commuting-square-transformation-cospan-Synthetic-Category-Theory κ μ H =
+    pr1 (pr2 (pr2 (pr2 H)))
+
+  right-commuting-square-transformation-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'}
+    (H : transformation-cospan-Synthetic-Category-Theory κ μ S S') →
+    commuting-square-functors-Synthetic-Category-Theory κ μ
+      ( right-functor-cospan-Synthetic-Category-Theory κ S)
+      ( middle-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+      ( right-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+      ( right-functor-cospan-Synthetic-Category-Theory κ S')
+  right-commuting-square-transformation-cospan-Synthetic-Category-Theory κ μ H =
+    pr2 (pr2 (pr2 (pr2 H)))
+```
+
+### Equivalences of cospans
+
+An equivalence of cospans S and S' is a transformations between S and S' such
+that all three vertical functors are equivalences.
+
+```agda
+module _
+  {l : Level}
+  where
+
+  equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    (S : cospan-Synthetic-Category-Theory κ C E D)
+    (S' : cospan-Synthetic-Category-Theory κ C' E' D') → UU l
+  equiv-cospan-Synthetic-Category-Theory κ μ ι S S' =
+    Σ ( equiv-Synthetic-Category-Theory κ μ ι
+        ( left-source-cospan-Synthetic-Category-Theory κ S)
+        ( left-source-cospan-Synthetic-Category-Theory κ S'))
+      ( λ φ →
+        Σ ( equiv-Synthetic-Category-Theory κ μ ι
+            ( target-cospan-Synthetic-Category-Theory κ S)
+            ( target-cospan-Synthetic-Category-Theory κ S'))
+          ( λ χ →
+            Σ ( equiv-Synthetic-Category-Theory κ μ ι
+                ( right-source-cospan-Synthetic-Category-Theory κ S)
+                ( right-source-cospan-Synthetic-Category-Theory κ S'))
+              ( λ ψ →
+                Σ ( commuting-square-functors-Synthetic-Category-Theory κ μ
+                    ( left-functor-cospan-Synthetic-Category-Theory κ S)
+                    ( functor-equiv-Synthetic-Category-Theory κ μ ι χ)
+                    ( functor-equiv-Synthetic-Category-Theory κ μ ι φ)
+                    ( left-functor-cospan-Synthetic-Category-Theory κ S'))
+                  ( λ τ →
+                    commuting-square-functors-Synthetic-Category-Theory κ μ
+                      ( right-functor-cospan-Synthetic-Category-Theory κ S)
+                      ( functor-equiv-Synthetic-Category-Theory κ μ ι χ)
+                      ( functor-equiv-Synthetic-Category-Theory κ μ ι ψ)
+                      ( right-functor-cospan-Synthetic-Category-Theory κ S')))))
+```
+
+### The components of an equivalence of cospans of synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  left-equiv-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    equiv-Synthetic-Category-Theory κ μ ι
+      ( left-source-cospan-Synthetic-Category-Theory κ S)
+      ( left-source-cospan-Synthetic-Category-Theory κ S')
+  left-equiv-equiv-cospan-Synthetic-Category-Theory κ μ ι H = pr1 H
+
+  left-functor-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    functor-Synthetic-Category-Theory κ
+      ( left-source-cospan-Synthetic-Category-Theory κ S)
+      ( left-source-cospan-Synthetic-Category-Theory κ S')
+  left-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    functor-equiv-Synthetic-Category-Theory κ μ ι
+      ( left-equiv-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+
+  middle-equiv-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    equiv-Synthetic-Category-Theory κ μ ι
+      ( target-cospan-Synthetic-Category-Theory κ S)
+      ( target-cospan-Synthetic-Category-Theory κ S')
+  middle-equiv-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    pr1 (pr2 H)
+
+  middle-functor-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    functor-Synthetic-Category-Theory κ
+      ( target-cospan-Synthetic-Category-Theory κ S)
+      ( target-cospan-Synthetic-Category-Theory κ S')
+  middle-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    functor-equiv-Synthetic-Category-Theory κ μ ι
+      ( middle-equiv-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+
+  right-equiv-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    equiv-Synthetic-Category-Theory κ μ ι
+      ( right-source-cospan-Synthetic-Category-Theory κ S)
+      ( right-source-cospan-Synthetic-Category-Theory κ S')
+  right-equiv-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    pr1 (pr2 (pr2 H))
+
+  right-functor-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    functor-Synthetic-Category-Theory κ
+      ( right-source-cospan-Synthetic-Category-Theory κ S)
+      ( right-source-cospan-Synthetic-Category-Theory κ S')
+  right-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    functor-equiv-Synthetic-Category-Theory κ μ ι
+      ( right-equiv-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+
+  left-commuting-square-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'}
+    (H : equiv-cospan-Synthetic-Category-Theory κ μ ι S S') →
+      ( commuting-square-functors-Synthetic-Category-Theory κ μ
+        ( left-functor-cospan-Synthetic-Category-Theory κ S)
+        ( middle-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+        ( left-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+        ( left-functor-cospan-Synthetic-Category-Theory κ S'))
+  left-commuting-square-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    pr1 (pr2 (pr2 (pr2 H)))
+
+  right-commuting-square-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'}
+    (H : equiv-cospan-Synthetic-Category-Theory κ μ ι S S') →
+      ( commuting-square-functors-Synthetic-Category-Theory κ μ
+        ( right-functor-cospan-Synthetic-Category-Theory κ S)
+        ( middle-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+        ( right-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H)
+        ( right-functor-cospan-Synthetic-Category-Theory κ S'))
+  right-commuting-square-equiv-cospan-Synthetic-Category-Theory κ μ ι H =
+    pr2 (pr2 (pr2 (pr2 H)))
+
+  transformation-cospan-equiv-cospan-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+    {S : cospan-Synthetic-Category-Theory κ C E D}
+    {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+    equiv-cospan-Synthetic-Category-Theory κ μ ι S S' →
+    transformation-cospan-Synthetic-Category-Theory κ μ S S'
+  pr1
+    ( transformation-cospan-equiv-cospan-Synthetic-Category-Theory κ μ ι H) =
+      left-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H
+  pr1 (pr2
+    ( transformation-cospan-equiv-cospan-Synthetic-Category-Theory κ μ ι H)) =
+      middle-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H
+  pr1 (pr2 (pr2
+    (transformation-cospan-equiv-cospan-Synthetic-Category-Theory κ μ ι H))) =
+      right-functor-equiv-cospan-Synthetic-Category-Theory κ μ ι H
+  pr1 (pr2 (pr2 (pr2
+    ( transformation-cospan-equiv-cospan-Synthetic-Category-Theory κ μ ι H)))) =
+      left-commuting-square-equiv-cospan-Synthetic-Category-Theory κ μ ι H
+  pr2 (pr2 (pr2 (pr2
+    ( transformation-cospan-equiv-cospan-Synthetic-Category-Theory κ μ ι H)))) =
+      right-commuting-square-equiv-cospan-Synthetic-Category-Theory κ μ ι H
+```
diff --git a/src/synthetic-category-theory/equivalence-of-synthetic-categories.lagda.md b/src/synthetic-category-theory/equivalence-of-synthetic-categories.lagda.md
deleted file mode 100644
index cba83e234f..0000000000
--- a/src/synthetic-category-theory/equivalence-of-synthetic-categories.lagda.md
+++ /dev/null
@@ -1,332 +0,0 @@
-# Equivalence of synthetic categories
-
-```agda
-{-# OPTIONS --guardedness #-}
-
-module synthetic-category-theory.equivalence-of-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.synthetic-categories
-```
-
-</details>
-
-## Definitions
-
-### Sections, retractions and equivalences
-
-Consider a functor f : C → D. A section of f is a functor s : D → C together
-with an isomorphism fs ≅ id_C. A retraction of f is a functor r : D → C together
-with an isomorphism rf ≅ id_D. The functor f is an equivalence if there is a
-functor g : D → C together with isomorphisms fg ≅ id_C and gf ≅ id_D.
-
-```agda
-module _
-  {l : Level}
-  where
-
-  is-section-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) →
-    (s : functor-Synthetic-Category-Theory κ D C) → UU l
-  is-section-Synthetic-Category-Theory κ μ ι C D f s =
-    isomorphism-Synthetic-Category-Theory
-      ( κ)
-      ( comp-functor-Synthetic-Category-Theory μ f s)
-      ( id-functor-Synthetic-Category-Theory ι D)
-
-  section-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) → UU l
-  section-Synthetic-Category-Theory κ μ ι C D f =
-    Σ ( functor-Synthetic-Category-Theory κ D C)
-      ( λ s → is-section-Synthetic-Category-Theory κ μ ι C D f s)
-
-  map-section-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) →
-    section-Synthetic-Category-Theory κ μ ι C D f →
-    functor-Synthetic-Category-Theory κ D C
-  map-section-Synthetic-Category-Theory κ μ ι C D f sec = pr1 sec
-
-  is-section-section-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) →
-    (sec : section-Synthetic-Category-Theory κ μ ι C D f) →
-    is-section-Synthetic-Category-Theory
-      κ μ ι C D f (map-section-Synthetic-Category-Theory κ μ ι C D f sec)
-  is-section-section-Synthetic-Category-Theory κ μ ι C D f sec = pr2 sec
-
-  is-retraction-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) →
-    (r : functor-Synthetic-Category-Theory κ D C) → UU l
-  is-retraction-Synthetic-Category-Theory κ μ ι C D f r =
-    isomorphism-Synthetic-Category-Theory
-      ( κ)
-      ( comp-functor-Synthetic-Category-Theory μ r f)
-      ( id-functor-Synthetic-Category-Theory ι C)
-
-  retraction-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) → UU l
-  retraction-Synthetic-Category-Theory κ μ ι C D f =
-    Σ ( functor-Synthetic-Category-Theory κ D C)
-      ( λ r → is-retraction-Synthetic-Category-Theory κ μ ι C D f r)
-
-  map-retraction-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) →
-    (retraction-Synthetic-Category-Theory κ μ ι C D f) →
-    (functor-Synthetic-Category-Theory κ D C)
-  map-retraction-Synthetic-Category-Theory κ μ ι C D f ret = pr1 ret
-
-  is-retraction-retraction-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) →
-    (ret : retraction-Synthetic-Category-Theory κ μ ι C D f) →
-    is-retraction-Synthetic-Category-Theory
-      κ μ ι C D f (map-retraction-Synthetic-Category-Theory κ μ ι C D f ret)
-  is-retraction-retraction-Synthetic-Category-Theory κ μ ι C D f ret = pr2 ret
-
-  is-equivalence-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)
-    (g : functor-Synthetic-Category-Theory κ D C) → UU l
-  is-equivalence-Synthetic-Category-Theory κ μ ι C D f g =
-        ( is-section-Synthetic-Category-Theory κ μ ι C D f g)
-          ×
-        ( is-retraction-Synthetic-Category-Theory κ μ ι C D f g)
-
-  equivalence-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) → UU l
-  equivalence-Synthetic-Category-Theory κ μ ι C D f =
-    Σ ( functor-Synthetic-Category-Theory κ D C)
-      ( λ g → is-equivalence-Synthetic-Category-Theory κ μ ι C D f g)
-
-  map-equivalence-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) →
-    equivalence-Synthetic-Category-Theory κ μ ι C D f →
-    functor-Synthetic-Category-Theory κ D C
-  map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq = pr1 eq
-
-  is-equivalence-equivalence-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) →
-    (eq : equivalence-Synthetic-Category-Theory κ μ ι C D f) →
-    is-equivalence-Synthetic-Category-Theory
-      κ μ ι C D f (map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq)
-  is-equivalence-equivalence-Synthetic-Category-Theory κ μ ι C D f eq = pr2 eq
-
-  is-section-equivalence-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) →
-    (eq : equivalence-Synthetic-Category-Theory κ μ ι C D f) →
-    is-section-Synthetic-Category-Theory
-      κ μ ι C D f (map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq)
-  is-section-equivalence-Synthetic-Category-Theory κ μ ι C D f eq =
-    pr1 (is-equivalence-equivalence-Synthetic-Category-Theory κ μ ι C D f eq)
-
-  is-retraction-equivalence-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) →
-    (eq : equivalence-Synthetic-Category-Theory κ μ ι C D f) →
-    is-retraction-Synthetic-Category-Theory
-      κ μ ι C D f (map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq)
-  is-retraction-equivalence-Synthetic-Category-Theory κ μ ι C D f eq =
-    pr2 (is-equivalence-equivalence-Synthetic-Category-Theory κ μ ι C D f eq)
-```
-
-A functor f : C → D admits a section and a retraction iff it is an equivalence
-(Lemma 1.1.6. in the book.)
-
-```agda
-  is-equivalence-admits-section-admits-retraction-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) →
-    equivalence-Synthetic-Category-Theory κ μ ι C D f →
-    (section-Synthetic-Category-Theory κ μ ι C D f)
-      ×
-    (retraction-Synthetic-Category-Theory κ μ ι C D f)
-  is-equivalence-admits-section-admits-retraction-Synthetic-Category-Theory
-    κ μ ι C D f eq =
-      ( map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq ,
-        pr1
-        (is-equivalence-equivalence-Synthetic-Category-Theory κ μ ι C D f eq)) ,
-      ( map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq ,
-        pr2
-        (is-equivalence-equivalence-Synthetic-Category-Theory κ μ ι C D f eq))
-
-  admits-section-admits-retraction-is-equivalence-Synthetic-Category-Theory :
-    (κ : language-Synthetic-Category-Theory l) →
-    (μ : composition-Synthetic-Category-Theory κ) →
-    (ι : identity-Synthetic-Category-Theory κ) →
-    (ν : inverse-Synthetic-Category-Theory κ) →
-    (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ) →
-    (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ) →
-    (X : horizontal-composition-Synthetic-Category-Theory κ μ) →
-    (Α : associative-composition-Synthetic-Category-Theory κ μ) →
-    (C D : category-Synthetic-Category-Theory κ) →
-    (f : functor-Synthetic-Category-Theory κ C D) →
-    section-Synthetic-Category-Theory κ μ ι C D f →
-    retraction-Synthetic-Category-Theory κ μ ι C D f →
-    equivalence-Synthetic-Category-Theory κ μ ι C D f
-  admits-section-admits-retraction-is-equivalence-Synthetic-Category-Theory
-    κ μ ι ν Λ Ρ Χ Α C D f sec ret =
-    let
-      s = map-section-Synthetic-Category-Theory κ μ ι C D f sec
-      Ξ = is-section-section-Synthetic-Category-Theory κ μ ι C D f sec
-      r = map-retraction-Synthetic-Category-Theory κ μ ι C D f ret
-      Ψ = is-retraction-retraction-Synthetic-Category-Theory κ μ ι C D f ret
-      α = comp-iso-Synthetic-Category-Theory μ
-          ( comp-iso-Synthetic-Category-Theory μ
-            ( comp-iso-Synthetic-Category-Theory μ
-              ( comp-iso-Synthetic-Category-Theory μ
-                ( right-unit-law-comp-functor-Synthetic-Category-Theory Ρ r)
-                ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-                  (id-iso-Synthetic-Category-Theory ι r) Ξ))
-              ( associative-comp-functor-Synthetic-Category-Theory Α r f s))
-            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-              ( inv-iso-Synthetic-Category-Theory ν Ψ)
-              ( id-iso-Synthetic-Category-Theory ι s)))
-            ( inv-iso-Synthetic-Category-Theory ν
-              ( left-unit-law-comp-functor-Synthetic-Category-Theory Λ s))
-      β = comp-iso-Synthetic-Category-Theory μ
-            ( Ψ)
-            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-              ( α)
-              ( id-iso-Synthetic-Category-Theory ι f))
-    in
-    s , Ξ , β
-```
-
-Equivalences are closed under composition (lemma 1.1.8.)
-
-```agda
-module _
-  {l : Level} {κ : language-Synthetic-Category-Theory l}
-  {μ : composition-Synthetic-Category-Theory κ}
-  {ι : identity-Synthetic-Category-Theory κ}
-  {ν : inverse-Synthetic-Category-Theory κ}
-  {Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ}
-  {Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ}
-  {Χ : horizontal-composition-Synthetic-Category-Theory κ μ}
-  {Α : associative-composition-Synthetic-Category-Theory κ μ}
-  where
-
-  equiv-equiv-comp-equiv-Synthetic-Category-Theory :
-    (C D E : category-Synthetic-Category-Theory κ) →
-    (f' : functor-Synthetic-Category-Theory κ D E) →
-    (f : functor-Synthetic-Category-Theory κ C D) →
-    (eq-f' : equivalence-Synthetic-Category-Theory κ μ ι D E f') →
-    (eq-f : equivalence-Synthetic-Category-Theory κ μ ι C D f) →
-    equivalence-Synthetic-Category-Theory
-      κ μ ι C E (comp-functor-Synthetic-Category-Theory μ f' f)
-  equiv-equiv-comp-equiv-Synthetic-Category-Theory
-    C D E f' f eq-f' eq-f =
-      let
-        g = map-equivalence-Synthetic-Category-Theory κ μ ι C D f eq-f
-        g' = map-equivalence-Synthetic-Category-Theory κ μ ι D E f' eq-f'
-      in
-      comp-functor-Synthetic-Category-Theory μ g g' ,
-      comp-iso-Synthetic-Category-Theory μ
-        ( is-section-equivalence-Synthetic-Category-Theory κ μ ι D E f' eq-f')
-        ( comp-iso-Synthetic-Category-Theory μ
-          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-            ( right-unit-law-comp-functor-Synthetic-Category-Theory Ρ f')
-            ( id-iso-Synthetic-Category-Theory ι g'))
-          ( comp-iso-Synthetic-Category-Theory μ
-            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-              ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-                ( id-iso-Synthetic-Category-Theory ι f')
-                ( is-section-equivalence-Synthetic-Category-Theory
-                  κ μ ι C D f eq-f))
-              ( id-iso-Synthetic-Category-Theory ι g'))
-            ( comp-iso-Synthetic-Category-Theory μ
-              ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-                ( associative-comp-functor-Synthetic-Category-Theory Α f' f g)
-                ( id-iso-Synthetic-Category-Theory ι g'))
-              ( inv-iso-Synthetic-Category-Theory ν
-                ( associative-comp-functor-Synthetic-Category-Theory Α
-                  ( comp-functor-Synthetic-Category-Theory μ f' f)
-                  ( g)
-                  ( g')))))) ,
-      comp-iso-Synthetic-Category-Theory μ
-        ( is-retraction-equivalence-Synthetic-Category-Theory κ μ ι C D f eq-f)
-        ( comp-iso-Synthetic-Category-Theory μ
-          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-            ( right-unit-law-comp-functor-Synthetic-Category-Theory Ρ g)
-            ( id-iso-Synthetic-Category-Theory ι f))
-          ( comp-iso-Synthetic-Category-Theory μ
-            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-              ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-                ( id-iso-Synthetic-Category-Theory ι g)
-                ( is-retraction-equivalence-Synthetic-Category-Theory
-                  κ μ ι D E f' eq-f'))
-              ( id-iso-Synthetic-Category-Theory ι f))
-            ( comp-iso-Synthetic-Category-Theory μ
-              ( horizontal-comp-iso-Synthetic-Category-Theory Χ
-                ( associative-comp-functor-Synthetic-Category-Theory Α g g' f')
-                ( id-iso-Synthetic-Category-Theory ι f))
-              ( inv-iso-Synthetic-Category-Theory ν
-                ( associative-comp-functor-Synthetic-Category-Theory Α
-                  ( comp-functor-Synthetic-Category-Theory μ g g')
-                  ( f')
-                  ( f))))))
-```
diff --git a/src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md b/src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..7e6f9d6866
--- /dev/null
+++ b/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)
+```
diff --git a/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md b/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..59b67d0c4f
--- /dev/null
+++ b/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md
@@ -0,0 +1,357 @@
+# Invertible functors between synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.invertible-functors-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.equivalences-synthetic-categories
+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
+{{#concept "invertible" Disambiguation="Synthetic categories"}} if it has an
+inverse, i.e. if there exists a functor g: B → A together with natural
+isomorphisms g∘f ≅ id and g∘f ≅ id.
+
+### The predicate of being an inverse to a functor f: A → B of synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-inverse-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)
+    (g : functor-Synthetic-Category-Theory κ D C) → UU l
+  is-inverse-Synthetic-Category-Theory κ μ ι f g =
+    ( is-section-Synthetic-Category-Theory κ μ ι f g)
+      ×
+    ( is-retraction-Synthetic-Category-Theory κ μ ι f g)
+```
+
+### The predicate of being an invertible functor of synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-invertible-functor-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) → UU l
+  is-invertible-functor-Synthetic-Category-Theory κ μ ι f =
+    Σ ( functor-Synthetic-Category-Theory κ _ _)
+      ( is-inverse-Synthetic-Category-Theory κ μ ι f)
+```
+
+### The type of invertible functors between two given synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  invertible-functor-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (C D : category-Synthetic-Category-Theory κ) → UU l
+  invertible-functor-Synthetic-Category-Theory κ μ ι C D =
+    Σ ( functor-Synthetic-Category-Theory κ C D)
+      ( is-invertible-functor-Synthetic-Category-Theory κ μ ι)
+```
+
+### The components of an invertible functor of synthetic categories
+
+```agda
+module _
+  {l : Level}
+  where
+
+  functor-invertible-functor-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    {C D : category-Synthetic-Category-Theory κ} →
+    invertible-functor-Synthetic-Category-Theory κ μ ι C D →
+    functor-Synthetic-Category-Theory κ C D
+  functor-invertible-functor-Synthetic-Category-Theory κ μ ι = pr1
+```
+
+### The components of a proof of being an invertible functor of synthetic categories
+
+```agda
+  inverse-functor-is-invertible-functor-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-invertible-functor-Synthetic-Category-Theory κ μ ι f →
+    functor-Synthetic-Category-Theory κ D C
+  inverse-functor-is-invertible-functor-Synthetic-Category-Theory κ μ ι = pr1
+
+  is-inverse-inverse-functor-is-invertible-functor-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}
+    (H : is-invertible-functor-Synthetic-Category-Theory κ μ ι f) →
+    is-inverse-Synthetic-Category-Theory κ μ ι f
+      ( inverse-functor-is-invertible-functor-Synthetic-Category-Theory κ μ ι H)
+  is-inverse-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+    κ μ ι =
+    pr2
+
+  is-section-inverse-functor-is-invertible-functor-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}
+    (H : is-invertible-functor-Synthetic-Category-Theory κ μ ι f) →
+    is-section-Synthetic-Category-Theory κ μ ι f
+      ( inverse-functor-is-invertible-functor-Synthetic-Category-Theory κ μ ι H)
+  is-section-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+    κ μ ι H =
+    pr1
+      ( is-inverse-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+        κ μ ι H)
+
+  is-retraction-inverse-functor-is-invertible-functor-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}
+    (H : is-invertible-functor-Synthetic-Category-Theory κ μ ι f) →
+    is-retraction-Synthetic-Category-Theory κ μ ι f
+      ( inverse-functor-is-invertible-functor-Synthetic-Category-Theory κ μ ι H)
+  is-retraction-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+    κ μ ι H =
+    pr2
+      ( is-inverse-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+        κ μ ι H)
+
+  section-is-invertible-functor-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-invertible-functor-Synthetic-Category-Theory κ μ ι f →
+    section-Synthetic-Category-Theory κ μ ι f
+  pr1 (section-is-invertible-functor-Synthetic-Category-Theory κ μ ι H) =
+    inverse-functor-is-invertible-functor-Synthetic-Category-Theory κ μ ι H
+  pr2 (section-is-invertible-functor-Synthetic-Category-Theory κ μ ι H) =
+    is-section-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+      κ μ ι H
+
+  retraction-is-invertible-functor-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-invertible-functor-Synthetic-Category-Theory κ μ ι f →
+    retraction-Synthetic-Category-Theory κ μ ι f
+  pr1 (retraction-is-invertible-functor-Synthetic-Category-Theory κ μ ι H) =
+    inverse-functor-is-invertible-functor-Synthetic-Category-Theory κ μ ι H
+  pr2 (retraction-is-invertible-functor-Synthetic-Category-Theory κ μ ι H) =
+    is-retraction-inverse-functor-is-invertible-functor-Synthetic-Category-Theory
+      κ μ ι H
+```
+
+### A functor f : C → D of synthetic categories is invertible iff it is an equivalence
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-equiv-is-invertible-functor-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-invertible-functor-Synthetic-Category-Theory κ μ ι f →
+    is-equiv-Synthetic-Category-Theory κ μ ι f
+  pr1 (is-equiv-is-invertible-functor-Synthetic-Category-Theory κ μ ι H) =
+    section-is-invertible-functor-Synthetic-Category-Theory κ μ ι H
+  pr2 (is-equiv-is-invertible-functor-Synthetic-Category-Theory κ μ ι H) =
+    retraction-is-invertible-functor-Synthetic-Category-Theory κ μ ι H
+
+  is-invertible-functor-is-equiv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (X : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    {C D : category-Synthetic-Category-Theory κ}
+    {f : functor-Synthetic-Category-Theory κ C D} →
+    is-equiv-Synthetic-Category-Theory κ μ ι f →
+    is-invertible-functor-Synthetic-Category-Theory κ μ ι f
+  pr1
+    ( is-invertible-functor-is-equiv-Synthetic-Category-Theory
+      κ μ ι ν Λ Ρ Χ Α B) =
+    functor-section-Synthetic-Category-Theory κ μ ι
+      ( section-is-equiv-Synthetic-Category-Theory κ μ ι B)
+  pr1 (pr2
+    ( is-invertible-functor-is-equiv-Synthetic-Category-Theory
+      κ μ ι ν Λ Ρ Χ Α B)) =
+    is-section-functor-section-Synthetic-Category-Theory κ μ ι
+      ( section-is-equiv-Synthetic-Category-Theory κ μ ι B)
+  pr2 (pr2
+    ( is-invertible-functor-is-equiv-Synthetic-Category-Theory
+      κ μ ι ν Λ Ρ Χ Α B)) =
+    comp-iso-Synthetic-Category-Theory μ
+      ( is-retraction-functor-retraction-Synthetic-Category-Theory κ μ ι
+        ( retraction-is-equiv-Synthetic-Category-Theory κ μ ι B))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+        ( comp-iso-Synthetic-Category-Theory μ
+          ( comp-iso-Synthetic-Category-Theory μ
+            ( comp-iso-Synthetic-Category-Theory μ
+              ( comp-iso-Synthetic-Category-Theory μ
+                ( right-unit-law-comp-functor-Synthetic-Category-Theory Ρ
+                  ( functor-retraction-Synthetic-Category-Theory κ μ ι
+                    ( retraction-is-equiv-Synthetic-Category-Theory κ μ ι B)))
+                ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                  ( id-iso-Synthetic-Category-Theory ι
+                    ( functor-retraction-Synthetic-Category-Theory κ μ ι
+                      ( retraction-is-equiv-Synthetic-Category-Theory κ μ ι B)))
+                  ( is-section-functor-section-Synthetic-Category-Theory κ μ ι
+                    ( section-is-equiv-Synthetic-Category-Theory κ μ ι B))))
+              ( associative-comp-functor-Synthetic-Category-Theory Α
+                ( functor-retraction-Synthetic-Category-Theory κ μ ι
+                  ( retraction-is-equiv-Synthetic-Category-Theory κ μ ι B))
+                ( _)
+                ( functor-section-Synthetic-Category-Theory κ μ ι
+                  ( section-is-equiv-Synthetic-Category-Theory κ μ ι B))))
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( inv-iso-Synthetic-Category-Theory ν
+                ( is-retraction-functor-retraction-Synthetic-Category-Theory
+                  κ μ ι
+                  ( retraction-is-equiv-Synthetic-Category-Theory κ μ ι B)))
+              ( id-iso-Synthetic-Category-Theory ι
+                ( functor-section-Synthetic-Category-Theory κ μ ι
+                  ( section-is-equiv-Synthetic-Category-Theory κ μ ι B)))))
+          ( inv-iso-Synthetic-Category-Theory ν
+            ( left-unit-law-comp-functor-Synthetic-Category-Theory Λ
+              ( functor-section-Synthetic-Category-Theory κ μ ι
+                ( section-is-equiv-Synthetic-Category-Theory κ μ ι B)))))
+        ( id-iso-Synthetic-Category-Theory ι _))
+```
+
+### Invertible functors of synthetic categories are closed under composition
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-invertible-functor-comp-is-invertible-functor-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    {C D E : category-Synthetic-Category-Theory κ}
+    {f' : functor-Synthetic-Category-Theory κ D E}
+    {f : functor-Synthetic-Category-Theory κ C D} →
+    is-invertible-functor-Synthetic-Category-Theory κ μ ι f' →
+    is-invertible-functor-Synthetic-Category-Theory κ μ ι f →
+    is-invertible-functor-Synthetic-Category-Theory κ μ ι
+      ( comp-functor-Synthetic-Category-Theory μ f' f)
+  pr1
+    ( is-invertible-functor-comp-is-invertible-functor-Synthetic-Category-Theory
+      κ μ ι ν Λ Ρ Χ Α K H) =
+    comp-functor-Synthetic-Category-Theory μ _ _
+  pr1 (pr2
+    ( is-invertible-functor-comp-is-invertible-functor-Synthetic-Category-Theory
+      κ μ ι ν Λ Ρ Χ Α K H)) =
+    comp-iso-Synthetic-Category-Theory μ
+      ( is-section-functor-section-Synthetic-Category-Theory κ μ ι
+        ( section-is-invertible-functor-Synthetic-Category-Theory κ μ ι K))
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( right-unit-law-comp-functor-Synthetic-Category-Theory Ρ _)
+          ( id-iso-Synthetic-Category-Theory ι
+            ( _)))
+        ( comp-iso-Synthetic-Category-Theory μ
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( id-iso-Synthetic-Category-Theory ι _)
+              ( is-section-functor-section-Synthetic-Category-Theory κ μ ι
+                ( section-is-invertible-functor-Synthetic-Category-Theory
+                  κ μ ι H)))
+            ( id-iso-Synthetic-Category-Theory ι _))
+          ( comp-iso-Synthetic-Category-Theory μ
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( associative-comp-functor-Synthetic-Category-Theory Α _ _ _)
+              ( id-iso-Synthetic-Category-Theory ι _))
+            ( inv-iso-Synthetic-Category-Theory ν
+              ( associative-comp-functor-Synthetic-Category-Theory Α
+                ( comp-functor-Synthetic-Category-Theory μ _ _)
+                ( _)
+                ( _))))))
+  pr2 (pr2
+    ( is-invertible-functor-comp-is-invertible-functor-Synthetic-Category-Theory
+      κ μ ι ν Λ Ρ Χ Α K H)) =
+    comp-iso-Synthetic-Category-Theory μ
+      ( is-retraction-functor-retraction-Synthetic-Category-Theory κ μ ι
+        ( retraction-is-invertible-functor-Synthetic-Category-Theory κ μ ι H))
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          ( right-unit-law-comp-functor-Synthetic-Category-Theory Ρ _)
+          ( id-iso-Synthetic-Category-Theory ι _))
+        ( comp-iso-Synthetic-Category-Theory μ
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( id-iso-Synthetic-Category-Theory ι _)
+              ( is-retraction-functor-retraction-Synthetic-Category-Theory κ μ ι
+                ( retraction-is-invertible-functor-Synthetic-Category-Theory
+                  κ μ ι K)))
+            ( id-iso-Synthetic-Category-Theory ι _))
+          ( comp-iso-Synthetic-Category-Theory μ
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( associative-comp-functor-Synthetic-Category-Theory Α _ _ _)
+              ( id-iso-Synthetic-Category-Theory ι _))
+            ( inv-iso-Synthetic-Category-Theory ν
+              ( associative-comp-functor-Synthetic-Category-Theory Α
+                ( comp-functor-Synthetic-Category-Theory μ _ _)
+                ( _)
+                ( _))))))
+```
diff --git a/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md b/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..9da94176ce
--- /dev/null
+++ b/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md
@@ -0,0 +1,285 @@
+# Pullbacks of synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.pullbacks-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.cone-diagrams-synthetic-categories
+open import synthetic-category-theory.cospans-synthetic-categories
+open import synthetic-category-theory.equivalences-synthetic-categories
+open import synthetic-category-theory.synthetic-categories
+```
+
+</details>
+
+## Idea
+
+Consider a
+[cospan diagram](synthetic-category-theory.cospans-synthetic-categories.md) S of
+[synthetic categories](synthetic-category-theory.synthetic-categories.md). The
+{{#concept "pullback" Disambiguation="Synthetic categories"}} of S is a cone
+diagram cᵤ = (pr₀, pr₁, τᵤ) over S with apex P that is universal in the sense
+that:
+
+```text
+1) for every cone diagram c = (t₀, t₁, τ) over S with apex T there exists a functor
+  (t₀, t₁) : T → P together with an isomorphism of cone diagrams c ≅ (t₀, t₁)*(cᵤ)
+2) given two functors f,g : T → P equipped with an isomorphism of cone diagrams
+  s*(cᵤ) ≅ t*(cᵤ), there exists a natural isomorphism s ≅ t that induces the said
+  isomorphism of cone diagrams.
+```
+
+```agda
+module _
+  {l : Level}
+  where
+
+  record
+    pullback-Synthetic-Category-Theory
+      (κ : language-Synthetic-Category-Theory l)
+      (μ : composition-Synthetic-Category-Theory κ)
+      (ι : identity-Synthetic-Category-Theory κ)
+      (ν : inverse-Synthetic-Category-Theory κ μ ι)
+      (Α : associative-composition-Synthetic-Category-Theory κ μ)
+      (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+      (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+      (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+      (Ξ :
+        preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+          κ μ Α Χ)
+      (I : interchange-composition-Synthetic-Category-Theory κ μ Χ)
+      (M :
+        preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ)
+      (N :
+        preserves-identity-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ) : UU l
+    where
+    coinductive
+    field
+      apex-pullback-Synthetic-Category-Theory :
+        {C D E : category-Synthetic-Category-Theory κ} →
+        cospan-Synthetic-Category-Theory κ C D E →
+          category-Synthetic-Category-Theory κ
+      cone-diagram-pullback-Synthetic-Category-Theory :
+        {C D E : category-Synthetic-Category-Theory κ}
+        (S : cospan-Synthetic-Category-Theory κ C D E) →
+          cone-diagram-Synthetic-Category-Theory
+            κ μ S ( apex-pullback-Synthetic-Category-Theory S)
+      universality-functor-pullback-Synthetic-Category-Theory :
+        {C D E : category-Synthetic-Category-Theory κ}
+        (S : cospan-Synthetic-Category-Theory κ C D E)
+        {T : category-Synthetic-Category-Theory κ}
+        (c : cone-diagram-Synthetic-Category-Theory κ μ S T) →
+          functor-Synthetic-Category-Theory κ
+            T ( apex-pullback-Synthetic-Category-Theory S)
+      universality-iso-pullback-Synthetic-Category-Theory :
+        {C D E : category-Synthetic-Category-Theory κ}
+        (S : cospan-Synthetic-Category-Theory κ C D E)
+        (T : category-Synthetic-Category-Theory κ)
+        (c : cone-diagram-Synthetic-Category-Theory κ μ S T) →
+          iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ
+          ( c)
+            ( induced-cone-diagram-Synthetic-Category-Theory κ μ ι ν Χ Α S
+              ( cone-diagram-pullback-Synthetic-Category-Theory S)
+              ( universality-functor-pullback-Synthetic-Category-Theory S c))
+      triviality-iso-of-cone-diagrams-pullback-Synthetic-Category-Theory :
+        {C D E : category-Synthetic-Category-Theory κ}
+        (S : cospan-Synthetic-Category-Theory κ C D E)
+        {T : category-Synthetic-Category-Theory κ}
+        (s t :
+          functor-Synthetic-Category-Theory κ T
+            ( apex-pullback-Synthetic-Category-Theory S))
+        (H : iso-of-cone-diagrams-Synthetic-Category-Theory κ μ ι Χ
+          (induced-cone-diagram-Synthetic-Category-Theory κ μ ι ν Χ Α S
+            ( cone-diagram-pullback-Synthetic-Category-Theory S)
+            ( s))
+          (induced-cone-diagram-Synthetic-Category-Theory κ μ ι ν Χ Α S
+            ( cone-diagram-pullback-Synthetic-Category-Theory S)
+            ( t))) →
+          Σ ( isomorphism-Synthetic-Category-Theory κ s t)
+            λ α →
+              iso-of-isos-of-cone-diagrams-Synthetic-Category-Theory κ μ ι ν Χ M
+                ( induced-iso-cone-diagram-Synthetic-Category-Theory
+                  κ μ ι ν Α Χ Λ Ρ Ξ I M N S
+                  ( cone-diagram-pullback-Synthetic-Category-Theory S)
+                  s t α)
+                ( H)
+
+open pullback-Synthetic-Category-Theory public
+```
+
+### The left and right projection functors with domain the apex of the pullback cone
+
+```agda
+module _
+  {l : Level}
+  where
+
+  left-functor-pullback-Synthetic-Category-Theory :
+      (κ : language-Synthetic-Category-Theory l)
+      (μ : composition-Synthetic-Category-Theory κ)
+      {ι : identity-Synthetic-Category-Theory κ}
+      {ν : inverse-Synthetic-Category-Theory κ μ ι}
+      {Α : associative-composition-Synthetic-Category-Theory κ μ}
+      {Χ : horizontal-composition-Synthetic-Category-Theory κ μ}
+      {Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ}
+      {Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ}
+      {Ξ :
+        preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+          κ μ Α Χ}
+      {I : interchange-composition-Synthetic-Category-Theory κ μ Χ}
+      {Μ :
+        preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ}
+      {Ν :
+        preserves-identity-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ}
+      (PB : pullback-Synthetic-Category-Theory κ μ ι ν Α Χ Λ Ρ Ξ I Μ Ν)
+      {C E D : category-Synthetic-Category-Theory κ}
+      (S : cospan-Synthetic-Category-Theory κ C E D) →
+      functor-Synthetic-Category-Theory κ
+        ( apex-pullback-Synthetic-Category-Theory PB S)
+        ( left-source-cospan-Synthetic-Category-Theory κ S)
+  left-functor-pullback-Synthetic-Category-Theory κ μ PB S =
+    left-functor-cone-diagram-Synthetic-Category-Theory κ μ
+      ( cone-diagram-pullback-Synthetic-Category-Theory PB S)
+
+  right-functor-pullback-Synthetic-Category-Theory :
+      (κ : language-Synthetic-Category-Theory l)
+      (μ : composition-Synthetic-Category-Theory κ)
+      {ι : identity-Synthetic-Category-Theory κ}
+      {ν : inverse-Synthetic-Category-Theory κ μ ι}
+      {Α : associative-composition-Synthetic-Category-Theory κ μ}
+      {Χ : horizontal-composition-Synthetic-Category-Theory κ μ}
+      {Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ}
+      {Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ}
+      {Ξ :
+        preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+          κ μ Α Χ}
+      {I : interchange-composition-Synthetic-Category-Theory κ μ Χ}
+      {Μ :
+        preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ}
+      {Ν :
+        preserves-identity-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ}
+      (PB : pullback-Synthetic-Category-Theory κ μ ι ν Α Χ Λ Ρ Ξ I Μ Ν)
+      {C E D : category-Synthetic-Category-Theory κ}
+      (S : cospan-Synthetic-Category-Theory κ C E D) →
+      functor-Synthetic-Category-Theory κ
+        ( apex-pullback-Synthetic-Category-Theory PB S)
+        ( right-source-cospan-Synthetic-Category-Theory κ S)
+  right-functor-pullback-Synthetic-Category-Theory κ μ PB S =
+    right-functor-cone-diagram-Synthetic-Category-Theory κ μ
+      ( cone-diagram-pullback-Synthetic-Category-Theory PB S)
+```
+
+### Functoriality of pullbacks
+
+Taking pullbacks is functorial in the sense that given cospans S and S' and a
+transformations of cospans S → S', there exists a preffered functor between the
+pullback of S and the pullback of S'.
+
+```agda
+module _
+  {l : Level}
+  where
+
+  functor-pullback-Synthetic-Category-Theory :
+      (κ : language-Synthetic-Category-Theory l)
+      (μ : composition-Synthetic-Category-Theory κ)
+      (ι : identity-Synthetic-Category-Theory κ)
+      (ν : inverse-Synthetic-Category-Theory κ μ ι)
+      (Α : associative-composition-Synthetic-Category-Theory κ μ)
+      (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+      {Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ}
+      {Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ}
+      {Ξ :
+        preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+          κ μ Α Χ}
+      {I : interchange-composition-Synthetic-Category-Theory κ μ Χ}
+      {M :
+        preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ}
+      {N :
+        preserves-identity-horizontal-composition-Synthetic-Category-Theory
+          κ ι μ Χ}
+      (PB : pullback-Synthetic-Category-Theory κ μ ι ν Α Χ Λ Ρ Ξ I M N)
+      {C C' E E' D D' : category-Synthetic-Category-Theory κ}
+      {S : cospan-Synthetic-Category-Theory κ C E D}
+      {S' : cospan-Synthetic-Category-Theory κ C' E' D'} →
+      transformation-cospan-Synthetic-Category-Theory κ μ S S' →
+      functor-Synthetic-Category-Theory κ
+        ( apex-pullback-Synthetic-Category-Theory PB S)
+        ( apex-pullback-Synthetic-Category-Theory PB S')
+  functor-pullback-Synthetic-Category-Theory
+    κ μ ι ν Α Χ PB {S = S} {S' = S'} H =
+    universality-functor-pullback-Synthetic-Category-Theory PB S'
+      ( comp-functor-Synthetic-Category-Theory μ
+        ( right-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+        ( right-functor-pullback-Synthetic-Category-Theory κ μ PB S) ,
+      ( comp-functor-Synthetic-Category-Theory μ
+        ( left-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+        ( left-functor-pullback-Synthetic-Category-Theory κ μ PB S)) ,
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( associative-comp-functor-Synthetic-Category-Theory Α
+          ( left-functor-cospan-Synthetic-Category-Theory κ S')
+          ( left-functor-transformation-cospan-Synthetic-Category-Theory κ μ H)
+          ( left-functor-pullback-Synthetic-Category-Theory κ μ PB S))
+        ( comp-iso-Synthetic-Category-Theory μ
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( left-commuting-square-transformation-cospan-Synthetic-Category-Theory
+              κ μ H)
+            ( id-iso-Synthetic-Category-Theory ι
+              ( left-functor-pullback-Synthetic-Category-Theory κ μ PB S)))
+          ( comp-iso-Synthetic-Category-Theory μ
+            ( inv-iso-Synthetic-Category-Theory ν
+              ( associative-comp-functor-Synthetic-Category-Theory Α
+                ( middle-functor-transformation-cospan-Synthetic-Category-Theory
+                  κ μ H)
+                ( left-functor-cospan-Synthetic-Category-Theory κ S)
+                ( left-functor-cone-diagram-Synthetic-Category-Theory κ μ
+                  ( cone-diagram-pullback-Synthetic-Category-Theory PB S))))
+            ( comp-iso-Synthetic-Category-Theory μ
+              ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                ( id-iso-Synthetic-Category-Theory ι
+                  ( middle-functor-transformation-cospan-Synthetic-Category-Theory
+                    κ μ H))
+                ( iso-cone-diagram-Synthetic-Category-Theory κ μ
+                  ( cone-diagram-pullback-Synthetic-Category-Theory PB S)))
+              ( comp-iso-Synthetic-Category-Theory μ
+                ( associative-comp-functor-Synthetic-Category-Theory Α
+                  ( middle-functor-transformation-cospan-Synthetic-Category-Theory
+                    κ μ H)
+                  ( right-functor-cospan-Synthetic-Category-Theory κ S)
+                  ( right-functor-pullback-Synthetic-Category-Theory κ μ PB S))
+                ( comp-iso-Synthetic-Category-Theory μ
+                  ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                    ( inv-iso-Synthetic-Category-Theory ν
+                      ( right-commuting-square-transformation-cospan-Synthetic-Category-Theory
+                        κ μ H))
+                    ( id-iso-Synthetic-Category-Theory ι
+                      ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ
+                        ( cone-diagram-pullback-Synthetic-Category-Theory PB
+                          S))))
+                  ( inv-iso-Synthetic-Category-Theory ν
+                    ( associative-comp-functor-Synthetic-Category-Theory Α
+                      ( right-functor-cospan-Synthetic-Category-Theory κ S')
+                      ( right-functor-transformation-cospan-Synthetic-Category-Theory
+                        κ μ H)
+                      ( right-functor-cone-diagram-Synthetic-Category-Theory κ μ
+                        ( cone-diagram-pullback-Synthetic-Category-Theory
+                          PB S)))))))))))
+```
diff --git a/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md b/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..cf22e0f544
--- /dev/null
+++ b/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md
@@ -0,0 +1,89 @@
+# Retractions of functors between synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.retractions-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.synthetic-categories
+```
+
+</details>
+
+## Idea
+
+A retraction of a functor f: A → B is a functor g: B → A equipped with a natural
+isomorphism g∘f ≅ id.
+
+### The predicate of being a retraction of a functor f: A → B
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-retraction-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) →
+    functor-Synthetic-Category-Theory κ D C → UU l
+  is-retraction-Synthetic-Category-Theory κ μ ι f r =
+    isomorphism-Synthetic-Category-Theory κ
+      ( comp-functor-Synthetic-Category-Theory μ r f)
+      ( id-functor-Synthetic-Category-Theory ι _)
+```
+
+### The type of retractions of a functor f: A → B
+
+```agda
+module _
+  {l : Level}
+  where
+
+  retraction-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) → UU l
+  retraction-Synthetic-Category-Theory κ μ ι f =
+    Σ ( functor-Synthetic-Category-Theory κ _ _)
+      ( is-retraction-Synthetic-Category-Theory κ μ ι f)
+```
+
+### The components of a retraction
+
+```agda
+  functor-retraction-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} →
+    retraction-Synthetic-Category-Theory κ μ ι f →
+      functor-Synthetic-Category-Theory κ D C
+  functor-retraction-Synthetic-Category-Theory κ μ ι = pr1
+
+  is-retraction-functor-retraction-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}
+    (r : retraction-Synthetic-Category-Theory κ μ ι f) →
+      is-retraction-Synthetic-Category-Theory κ μ ι f
+        ( functor-retraction-Synthetic-Category-Theory κ μ ι r)
+  is-retraction-functor-retraction-Synthetic-Category-Theory κ μ ι = pr2
+```
diff --git a/src/synthetic-category-theory/sections-synthetic-categories.lagda.md b/src/synthetic-category-theory/sections-synthetic-categories.lagda.md
new file mode 100644
index 0000000000..acd4f1c5db
--- /dev/null
+++ b/src/synthetic-category-theory/sections-synthetic-categories.lagda.md
@@ -0,0 +1,89 @@
+# Sections of functor between synthetic categories
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module synthetic-category-theory.sections-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.synthetic-categories
+```
+
+</details>
+
+## Idea
+
+A section of a functor f: A → B is a functor g: B → A equipped with a natural
+isomorphism f∘g ≅ id.
+
+### The predicate of being a section of a functor f: A → B
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-section-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) →
+    functor-Synthetic-Category-Theory κ D C → UU l
+  is-section-Synthetic-Category-Theory κ μ ι f s =
+    isomorphism-Synthetic-Category-Theory κ
+      ( comp-functor-Synthetic-Category-Theory μ f s)
+      ( id-functor-Synthetic-Category-Theory ι _)
+```
+
+### The type of sections of a funcor f: A → B
+
+```agda
+module _
+  {l : Level}
+  where
+
+  section-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) → UU l
+  section-Synthetic-Category-Theory κ μ ι f =
+    Σ ( functor-Synthetic-Category-Theory κ _ _)
+      ( is-section-Synthetic-Category-Theory κ μ ι f)
+```
+
+### The components of a section
+
+```agda
+  functor-section-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} →
+    section-Synthetic-Category-Theory κ μ ι f →
+      functor-Synthetic-Category-Theory κ D C
+  functor-section-Synthetic-Category-Theory κ μ ι = pr1
+
+  is-section-functor-section-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}
+    (s : section-Synthetic-Category-Theory κ μ ι f) →
+      is-section-Synthetic-Category-Theory κ μ ι f
+        ( functor-section-Synthetic-Category-Theory κ μ ι s)
+  is-section-functor-section-Synthetic-Category-Theory κ μ ι = pr2
+```
diff --git a/src/synthetic-category-theory/synthetic-categories.lagda.md b/src/synthetic-category-theory/synthetic-categories.lagda.md
index e161385fc9..80066da1ba 100644
--- a/src/synthetic-category-theory/synthetic-categories.lagda.md
+++ b/src/synthetic-category-theory/synthetic-categories.lagda.md
@@ -107,6 +107,28 @@ module _
   functor-Synthetic-Category-Theory = 1-cell-Globular-Type
 ```
 
+#### The source and target of a functor
+
+```agda
+module _
+  {l : Level}
+  where
+
+  source-functor-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D : category-Synthetic-Category-Theory κ} →
+    functor-Synthetic-Category-Theory κ C D →
+    category-Synthetic-Category-Theory κ
+  source-functor-Synthetic-Category-Theory κ {C = C} f = C
+
+  target-functor-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D : category-Synthetic-Category-Theory κ} →
+    functor-Synthetic-Category-Theory κ C D →
+    category-Synthetic-Category-Theory κ
+  target-functor-Synthetic-Category-Theory κ {D = D} f = D
+```
+
 #### The globular type of functors between categories
 
 The globular type of functors from `C` to `D` in the language of synthetic
@@ -125,7 +147,7 @@ module _
     1-cell-globular-type-Globular-Type
 ```
 
-#### The sort of isomorphisms between functors in the language of synthetic category theory
+#### The sort of isomorphisms between functors in the language ofsynthetic category theory
 
 The sort of isomorphisms between functors `F` and `G` in the language of
 synthetic category theory is the type of `2`-cells between `F` and `G` in the
@@ -143,28 +165,19 @@ module _
   isomorphism-Synthetic-Category-Theory = 2-cell-Globular-Type
 ```
 
-#### Inverses of isomorphisms
-
-Isomorphisms between functors, as well as higher isomorphisms, are invertible.
+#### Isomorphism between isomorphisms between functors in the language of synthetic category theory
 
 ```agda
 module _
   {l : Level}
   where
 
-  record
-    inverse-Synthetic-Category-Theory
-      (κ : language-Synthetic-Category-Theory l) : UU l
-    where
-    coinductive
-    field
-      inv-iso-Synthetic-Category-Theory :
-        {C D : category-Synthetic-Category-Theory κ} →
-        {F G : functor-Synthetic-Category-Theory κ C D} →
-        (isomorphism-Synthetic-Category-Theory κ F G) →
-        (isomorphism-Synthetic-Category-Theory κ G F)
-
-  open inverse-Synthetic-Category-Theory public
+  3-isomorphism-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    {C D : category-Synthetic-Category-Theory κ}
+    {F G : functor-Synthetic-Category-Theory κ C D}
+    (α β : isomorphism-Synthetic-Category-Theory κ F G) → UU l
+  3-isomorphism-Synthetic-Category-Theory = 3-cell-Globular-Type
 ```
 
 #### The structure of identity morphisms in the language of synthetic category theory
@@ -249,6 +262,56 @@ module _
       ( composition-isomorphism-Synthetic-Category-Theory μ)
 ```
 
+#### Inverses of isomorphisms
+
+Isomorphisms between functors, as well as higher isomorphisms, are invertible.
+
+```agda
+module _
+  {l : Level}
+  where
+
+  record
+    inverse-Synthetic-Category-Theory
+      (κ : language-Synthetic-Category-Theory l)
+      (μ : composition-Synthetic-Category-Theory κ)
+      (ι : identity-Synthetic-Category-Theory κ) : UU l
+    where
+    coinductive
+    field
+      inv-iso-Synthetic-Category-Theory :
+        {C D : category-Synthetic-Category-Theory κ} →
+        {F G : functor-Synthetic-Category-Theory κ C D} →
+        (isomorphism-Synthetic-Category-Theory κ F G) →
+        (isomorphism-Synthetic-Category-Theory κ G F)
+      inv-iso-left-inv-Synthetic-Category-Theory :
+        {C D : category-Synthetic-Category-Theory κ} →
+        {F G : functor-Synthetic-Category-Theory κ C D} →
+        (α : isomorphism-Synthetic-Category-Theory κ F G) →
+        isomorphism-Synthetic-Category-Theory
+          ( functor-globular-type-Synthetic-Category-Theory κ C D)
+          ( comp-iso-Synthetic-Category-Theory μ
+            ( inv-iso-Synthetic-Category-Theory α) α)
+            ( id-iso-Synthetic-Category-Theory ι F)
+      inv-iso-right-inv-Synthetic-Category-Theory :
+        {C D : category-Synthetic-Category-Theory κ} →
+        {F G : functor-Synthetic-Category-Theory κ C D} →
+        (α : isomorphism-Synthetic-Category-Theory κ F G) →
+        isomorphism-Synthetic-Category-Theory
+          ( functor-globular-type-Synthetic-Category-Theory κ C D)
+          ( comp-iso-Synthetic-Category-Theory μ
+            α ( inv-iso-Synthetic-Category-Theory α))
+            ( id-iso-Synthetic-Category-Theory ι G)
+      inverse-isomorphism-Synthetic-Category-Theory :
+        {C D : category-Synthetic-Category-Theory κ} →
+        inverse-Synthetic-Category-Theory
+          ( functor-globular-type-Synthetic-Category-Theory κ C D)
+          ( composition-isomorphism-Synthetic-Category-Theory μ)
+          ( identity-isomorphism-Synthetic-Category-Theory ι)
+
+  open inverse-Synthetic-Category-Theory public
+```
+
 #### Left unit law operators in the language of synthetic category theory
 
 ```agda
@@ -378,6 +441,75 @@ module _
   open horizontal-composition-Synthetic-Category-Theory public
 ```
 
+#### We can prove that taking an inverse is an idempotent operation
+
+```agda
+module _
+  {l : Level}
+  where
+
+  inverse-idempotent-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    {C D : category-Synthetic-Category-Theory κ}
+    {F G : functor-Synthetic-Category-Theory κ C D}
+    (α : isomorphism-Synthetic-Category-Theory κ F G) →
+    isomorphism-Synthetic-Category-Theory
+      ( functor-globular-type-Synthetic-Category-Theory κ C D)
+      ( inv-iso-Synthetic-Category-Theory ν
+        ( inv-iso-Synthetic-Category-Theory ν α))
+      ( α)
+  inverse-idempotent-Synthetic-Category-Theory κ μ ι ν Α Χ Λ Ρ α =
+    comp-iso-Synthetic-Category-Theory
+      ( composition-isomorphism-Synthetic-Category-Theory μ)
+      ( left-unit-law-comp-functor-Synthetic-Category-Theory
+        ( left-unit-law-composition-isomorphism-Synthetic-Category-Theory Λ)
+        ( α))
+      ( comp-iso-Synthetic-Category-Theory
+        ( composition-isomorphism-Synthetic-Category-Theory μ)
+        ( horizontal-comp-iso-Synthetic-Category-Theory
+          ( horizontal-composition-isomorphism-Synthetic-Category-Theory Χ)
+          ( inv-iso-left-inv-Synthetic-Category-Theory ν
+            ( inv-iso-Synthetic-Category-Theory ν α))
+          ( id-iso-Synthetic-Category-Theory
+            ( identity-isomorphism-Synthetic-Category-Theory ι)
+            ( α)))
+        ( comp-iso-Synthetic-Category-Theory
+          ( composition-isomorphism-Synthetic-Category-Theory μ)
+          ( inv-iso-Synthetic-Category-Theory
+            ( inverse-isomorphism-Synthetic-Category-Theory ν)
+            ( associative-comp-functor-Synthetic-Category-Theory
+              ( associative-comp-isomorphism-Synthetic-Category-Theory Α)
+              ( inv-iso-Synthetic-Category-Theory ν
+                ( inv-iso-Synthetic-Category-Theory ν α))
+              ( inv-iso-Synthetic-Category-Theory ν α)
+              ( α)))
+          ( comp-iso-Synthetic-Category-Theory
+            ( composition-isomorphism-Synthetic-Category-Theory μ)
+            ( horizontal-comp-iso-Synthetic-Category-Theory
+              ( horizontal-composition-isomorphism-Synthetic-Category-Theory Χ)
+              ( id-iso-Synthetic-Category-Theory
+                ( identity-isomorphism-Synthetic-Category-Theory ι)
+                ( inv-iso-Synthetic-Category-Theory ν
+                  ( inv-iso-Synthetic-Category-Theory ν α)))
+              ( inv-iso-Synthetic-Category-Theory
+                ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                ( inv-iso-left-inv-Synthetic-Category-Theory ν α)))
+            ( inv-iso-Synthetic-Category-Theory
+              ( inverse-isomorphism-Synthetic-Category-Theory ν)
+              ( right-unit-law-comp-functor-Synthetic-Category-Theory
+                ( right-unit-law-composition-isomorphism-Synthetic-Category-Theory
+                  Ρ)
+                ( inv-iso-Synthetic-Category-Theory ν
+                  ( inv-iso-Synthetic-Category-Theory ν α)))))))
+```
+
 #### Identity preservation operators for horizontal composition in the language of synthetic category theory
 
 ```agda
@@ -500,7 +632,54 @@ module _
       ( comp-functor-Synthetic-Category-Theory μ g i)
 ```
 
-#### Commuting squares of isomorphisms in the language of synthetic category theory
+#### Pasting of commutative squares of functors
+
+```agda
+module _
+  {l : Level}
+  where
+
+  pasting-commuting-squares-functors-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (α : associative-composition-Synthetic-Category-Theory κ μ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    {A B C X Y Z : category-Synthetic-Category-Theory κ}
+    (f : functor-Synthetic-Category-Theory κ A B)
+    (g : functor-Synthetic-Category-Theory κ B C)
+    (h : functor-Synthetic-Category-Theory κ C Z)
+    (r : functor-Synthetic-Category-Theory κ A X)
+    (s : functor-Synthetic-Category-Theory κ X Y)
+    (t : functor-Synthetic-Category-Theory κ Y Z)
+    (u : functor-Synthetic-Category-Theory κ B Y) →
+    (commuting-square-functors-Synthetic-Category-Theory κ μ f u r s) →
+    (commuting-square-functors-Synthetic-Category-Theory κ μ g h u t) →
+    commuting-square-functors-Synthetic-Category-Theory κ μ
+      ( comp-functor-Synthetic-Category-Theory μ g f)
+      ( h)
+      ( r)
+      ( comp-functor-Synthetic-Category-Theory μ t s)
+  pasting-commuting-squares-functors-Synthetic-Category-Theory
+    κ μ ι ν α Χ f g h r s t u τ σ =
+    comp-iso-Synthetic-Category-Theory μ
+      ( inv-iso-Synthetic-Category-Theory ν
+        ( associative-comp-functor-Synthetic-Category-Theory α t s r))
+      ( comp-iso-Synthetic-Category-Theory μ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+          (id-iso-Synthetic-Category-Theory ι t) τ)
+        ( comp-iso-Synthetic-Category-Theory μ
+          ( associative-comp-functor-Synthetic-Category-Theory α t u f)
+          ( comp-iso-Synthetic-Category-Theory μ
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+              ( σ)
+              ( id-iso-Synthetic-Category-Theory ι f))
+            ( inv-iso-Synthetic-Category-Theory ν
+              ( associative-comp-functor-Synthetic-Category-Theory α h g f)))))
+```
+
+#### Commutative squares of isomorphisms in the language of synthetic category theory
 
 ```agda
 module _
@@ -522,6 +701,46 @@ module _
       ( composition-isomorphism-Synthetic-Category-Theory μ)
 ```
 
+#### Pasting commutative squares of isomorphisms
+
+```agda
+module _
+  {l : Level}
+  where
+
+  pasting-commuting-squares-isomorphisms-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    {C D : category-Synthetic-Category-Theory κ}
+    {f g h r s t : functor-Synthetic-Category-Theory κ C D}
+    (α : isomorphism-Synthetic-Category-Theory κ f g)
+    (β : isomorphism-Synthetic-Category-Theory κ g h)
+    (γ : isomorphism-Synthetic-Category-Theory κ h t)
+    (δ : isomorphism-Synthetic-Category-Theory κ f r)
+    (ε : isomorphism-Synthetic-Category-Theory κ r s)
+    (φ : isomorphism-Synthetic-Category-Theory κ s t)
+    (ξ : isomorphism-Synthetic-Category-Theory κ g s) →
+    (commuting-square-isomorphisms-Synthetic-Category-Theory κ μ α ξ δ ε) →
+    (commuting-square-isomorphisms-Synthetic-Category-Theory κ μ β γ ξ φ) →
+    commuting-square-isomorphisms-Synthetic-Category-Theory κ μ
+      ( comp-iso-Synthetic-Category-Theory μ β α)
+      ( γ)
+      ( δ)
+      ( comp-iso-Synthetic-Category-Theory μ φ ε)
+  pasting-commuting-squares-isomorphisms-Synthetic-Category-Theory κ μ ι ν Α Χ =
+    pasting-commuting-squares-functors-Synthetic-Category-Theory
+      ( functor-globular-type-Synthetic-Category-Theory κ _ _)
+      ( composition-isomorphism-Synthetic-Category-Theory μ)
+      ( identity-isomorphism-Synthetic-Category-Theory ι)
+      ( inverse-isomorphism-Synthetic-Category-Theory ν)
+      ( associative-comp-isomorphism-Synthetic-Category-Theory Α)
+      ( horizontal-composition-isomorphism-Synthetic-Category-Theory Χ)
+```
+
 #### Left unit law preservation operators for horizontal composition
 
 ```agda
@@ -559,6 +778,10 @@ module _
           ( composition-isomorphism-Synthetic-Category-Theory μ)
           ( left-unit-law-composition-isomorphism-Synthetic-Category-Theory η)
           ( horizontal-composition-isomorphism-Synthetic-Category-Theory ν)
+
+open
+    preserves-left-unit-law-composition-horizontal-composition-Synthetic-Category-Theory
+      public
 ```
 
 #### Right unit law preservation operators for horizontal composition
@@ -598,6 +821,10 @@ module _
           ( composition-isomorphism-Synthetic-Category-Theory μ)
           ( right-unit-law-composition-isomorphism-Synthetic-Category-Theory η)
           ( horizontal-composition-isomorphism-Synthetic-Category-Theory ν)
+
+open
+    preserves-right-unit-law-composition-horizontal-composition-Synthetic-Category-Theory
+      public
 ```
 
 #### Associator preservation operators for horizontal composition
@@ -633,4 +860,226 @@ module _
             ( horizontal-comp-iso-Synthetic-Category-Theory ν γ β)
             ( α))
           ( associative-comp-functor-Synthetic-Category-Theory η H' G' F')
+
+open
+    preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+      public
+```
+
+#### We can prove that the inverse of the associator preservers horizontal composition
+
+```agda
+module _
+  {l : Level}
+  where
+
+  preserves-associativity-comp-functor-horizontal-comp-iso-inv-Synthetic-Category-Theory :
+    (κ : language-Synthetic-Category-Theory l)
+    (μ : composition-Synthetic-Category-Theory κ)
+    (ι : identity-Synthetic-Category-Theory κ)
+    (ν : inverse-Synthetic-Category-Theory κ μ ι)
+    (Α : associative-composition-Synthetic-Category-Theory κ μ)
+    (Χ : horizontal-composition-Synthetic-Category-Theory κ μ)
+    (Λ : left-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ρ : right-unit-law-composition-Synthetic-Category-Theory κ ι μ)
+    (Ξ :
+        preserves-associativity-composition-horizontal-composition-Synthetic-Category-Theory
+          κ μ Α Χ)
+    {C1 C2 C3 C4 : category-Synthetic-Category-Theory κ}
+    (H H' : functor-Synthetic-Category-Theory κ C3 C4)
+    (G G' : functor-Synthetic-Category-Theory κ C2 C3)
+    (F F' : functor-Synthetic-Category-Theory κ C1 C2)
+    (γ : isomorphism-Synthetic-Category-Theory κ H H')
+    (β : isomorphism-Synthetic-Category-Theory κ G G')
+    (α : isomorphism-Synthetic-Category-Theory κ F F') →
+    commuting-square-isomorphisms-Synthetic-Category-Theory κ μ
+      ( inv-iso-Synthetic-Category-Theory ν
+        ( associative-comp-functor-Synthetic-Category-Theory Α H G F))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ β)
+        ( α))
+      ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ
+        ( horizontal-comp-iso-Synthetic-Category-Theory Χ β α))
+      ( inv-iso-Synthetic-Category-Theory ν
+        ( associative-comp-functor-Synthetic-Category-Theory Α H' G' F'))
+  preserves-associativity-comp-functor-horizontal-comp-iso-inv-Synthetic-Category-Theory
+    κ μ ι ν Α Χ Λ Ρ Ξ H H' G G' F F' γ β α =
+    comp-iso-Synthetic-Category-Theory
+      ( composition-isomorphism-Synthetic-Category-Theory μ)
+      ( right-unit-law-comp-functor-Synthetic-Category-Theory
+        ( right-unit-law-composition-isomorphism-Synthetic-Category-Theory Ρ)
+        ( comp-iso-Synthetic-Category-Theory μ
+          ( inv-iso-Synthetic-Category-Theory ν
+            ( associative-comp-functor-Synthetic-Category-Theory Α H' G' F'))
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+            ( γ)
+            ( horizontal-comp-iso-Synthetic-Category-Theory Χ β α))))
+      ( comp-iso-Synthetic-Category-Theory
+        ( composition-isomorphism-Synthetic-Category-Theory μ)
+        ( horizontal-comp-iso-Synthetic-Category-Theory
+          ( horizontal-composition-isomorphism-Synthetic-Category-Theory Χ)
+          ( id-iso-Synthetic-Category-Theory
+            ( identity-isomorphism-Synthetic-Category-Theory ι)
+            ( comp-iso-Synthetic-Category-Theory μ
+              ( inv-iso-Synthetic-Category-Theory ν
+                ( associative-comp-functor-Synthetic-Category-Theory
+                  Α H' G' F'))
+              ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ
+                ( horizontal-comp-iso-Synthetic-Category-Theory Χ β α))))
+          ( inv-iso-right-inv-Synthetic-Category-Theory ν
+            ( associative-comp-functor-Synthetic-Category-Theory Α H G F)))
+        ( comp-iso-Synthetic-Category-Theory
+          ( composition-isomorphism-Synthetic-Category-Theory μ)
+          ( associative-comp-functor-Synthetic-Category-Theory
+            ( associative-comp-isomorphism-Synthetic-Category-Theory Α)
+            ( comp-iso-Synthetic-Category-Theory μ
+              ( inv-iso-Synthetic-Category-Theory ν
+                ( associative-comp-functor-Synthetic-Category-Theory
+                  Α H' G' F'))
+              ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                ( γ)
+                ( horizontal-comp-iso-Synthetic-Category-Theory Χ β α)))
+            ( associative-comp-functor-Synthetic-Category-Theory Α H G F)
+            ( inv-iso-Synthetic-Category-Theory ν
+              ( associative-comp-functor-Synthetic-Category-Theory Α H G F)))
+          ( comp-iso-Synthetic-Category-Theory
+            ( composition-isomorphism-Synthetic-Category-Theory μ)
+            ( horizontal-comp-iso-Synthetic-Category-Theory
+              ( horizontal-composition-isomorphism-Synthetic-Category-Theory Χ)
+              ( inv-iso-Synthetic-Category-Theory
+                ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                ( associative-comp-functor-Synthetic-Category-Theory
+                  ( associative-comp-isomorphism-Synthetic-Category-Theory Α)
+                  ( inv-iso-Synthetic-Category-Theory ν
+                    ( associative-comp-functor-Synthetic-Category-Theory
+                      Α H' G' F'))
+                  ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                    ( γ)
+                    ( horizontal-comp-iso-Synthetic-Category-Theory Χ β α))
+                  ( associative-comp-functor-Synthetic-Category-Theory
+                    Α H G F)))
+              ( id-iso-Synthetic-Category-Theory
+                ( identity-isomorphism-Synthetic-Category-Theory ι)
+                ( inv-iso-Synthetic-Category-Theory ν
+                  ( associative-comp-functor-Synthetic-Category-Theory
+                    Α H G F))))
+            ( comp-iso-Synthetic-Category-Theory
+              ( composition-isomorphism-Synthetic-Category-Theory μ)
+              ( horizontal-comp-iso-Synthetic-Category-Theory
+                ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                  Χ)
+                ( horizontal-comp-iso-Synthetic-Category-Theory
+                  ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                    Χ)
+                  ( id-iso-Synthetic-Category-Theory
+                    ( identity-isomorphism-Synthetic-Category-Theory ι)
+                    ( inv-iso-Synthetic-Category-Theory ν
+                    ( associative-comp-functor-Synthetic-Category-Theory
+                      Α H' G' F')))
+                  ( inv-iso-Synthetic-Category-Theory
+                    ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                    ( preserves-associativity-comp-functor-horizontal-comp-iso-Synthetic-Category-Theory
+                      Ξ γ β α)))
+                ( id-iso-Synthetic-Category-Theory
+                  ( identity-isomorphism-Synthetic-Category-Theory ι)
+                  ( inv-iso-Synthetic-Category-Theory ν
+                    ( associative-comp-functor-Synthetic-Category-Theory
+                      Α H G F))))
+              ( comp-iso-Synthetic-Category-Theory
+                ( composition-isomorphism-Synthetic-Category-Theory μ)
+                ( horizontal-comp-iso-Synthetic-Category-Theory
+                  ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                    Χ)
+                  ( associative-comp-functor-Synthetic-Category-Theory
+                    ( associative-comp-isomorphism-Synthetic-Category-Theory Α)
+                    ( inv-iso-Synthetic-Category-Theory ν
+                      ( associative-comp-functor-Synthetic-Category-Theory
+                        Α H' G' F'))
+                    ( associative-comp-functor-Synthetic-Category-Theory
+                      Α H' G' F')
+                    ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                      ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ β)
+                      ( α)))
+                  ( id-iso-Synthetic-Category-Theory
+                    ( identity-isomorphism-Synthetic-Category-Theory ι)
+                    ( inv-iso-Synthetic-Category-Theory ν
+                      ( associative-comp-functor-Synthetic-Category-Theory
+                        Α H G F))))
+                ( comp-iso-Synthetic-Category-Theory
+                  ( composition-isomorphism-Synthetic-Category-Theory μ)
+                  ( horizontal-comp-iso-Synthetic-Category-Theory
+                    ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                      Χ)
+                    ( horizontal-comp-iso-Synthetic-Category-Theory
+                      ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                        Χ)
+                      ( inv-iso-Synthetic-Category-Theory
+                        ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                        ( inv-iso-left-inv-Synthetic-Category-Theory ν
+                          ( associative-comp-functor-Synthetic-Category-Theory
+                            Α H' G' F')))
+                      ( id-iso-Synthetic-Category-Theory
+                        ( identity-isomorphism-Synthetic-Category-Theory ι)
+                        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                          ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ β)
+                            (α))))
+                    ( id-iso-Synthetic-Category-Theory
+                      ( identity-isomorphism-Synthetic-Category-Theory ι)
+                      ( inv-iso-Synthetic-Category-Theory ν
+                        ( associative-comp-functor-Synthetic-Category-Theory
+                          Α H G F))))
+                  ( horizontal-comp-iso-Synthetic-Category-Theory
+                    ( horizontal-composition-isomorphism-Synthetic-Category-Theory
+                      Χ)
+                    ( inv-iso-Synthetic-Category-Theory
+                      ( inverse-isomorphism-Synthetic-Category-Theory ν)
+                      ( left-unit-law-comp-functor-Synthetic-Category-Theory
+                        ( left-unit-law-composition-isomorphism-Synthetic-Category-Theory
+                          Λ)
+                        ( horizontal-comp-iso-Synthetic-Category-Theory Χ
+                          ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ β)
+                          ( α))))
+                    ( id-iso-Synthetic-Category-Theory
+                      ( identity-isomorphism-Synthetic-Category-Theory ι)
+                      ( inv-iso-Synthetic-Category-Theory ν
+                        ( associative-comp-functor-Synthetic-Category-Theory
+                          Α H G F))))))))))
+```
+
+#### Preservation of isomorphisms of natural isomorphisms by horizontal composition
+
+We have to assume as an additional axiom that given natural isomorphism α, α',
+β, β' with appropriate domains and codomains, together with isomorphisms α ≅ α'
+and β ≅ β', there exists an isomorphisms between the horizontal composites β _ α
+≅ β' _ α'.
+
+```agda
+module _
+  {l : Level}
+  where
+
+  record
+    preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+      (κ : language-Synthetic-Category-Theory l)
+      (ι : identity-Synthetic-Category-Theory κ)
+      (μ : composition-Synthetic-Category-Theory κ)
+      (Χ : horizontal-composition-Synthetic-Category-Theory κ μ) : UU l
+    where
+    coinductive
+    field
+      preserves-isomorphism-horizontal-comp-iso-Synthetic-Category-Theory :
+        {C D E : category-Synthetic-Category-Theory κ}
+        {F F' : functor-Synthetic-Category-Theory κ C D}
+        {G G' : functor-Synthetic-Category-Theory κ D E}
+        {α β : isomorphism-Synthetic-Category-Theory κ F F'}
+        {γ δ : isomorphism-Synthetic-Category-Theory κ G G'} →
+        3-isomorphism-Synthetic-Category-Theory κ α β →
+        3-isomorphism-Synthetic-Category-Theory κ γ δ →
+        3-isomorphism-Synthetic-Category-Theory κ
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ γ α)
+          ( horizontal-comp-iso-Synthetic-Category-Theory Χ δ β)
+
+open
+  preserves-isomorphism-horizontal-composition-Synthetic-Category-Theory
+    public
 ```