From a85a1d059db74c2116e149e53de30285b97c13ab Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Mar 2024 11:39:30 +0100
Subject: [PATCH 1/2] sections and retractions in (large) (pre)categories

---
 .../retractions-in-categories.lagda.md        | 67 ++++++++++++++++
 .../retractions-in-large-categories.lagda.md  | 78 +++++++++++++++++++
 ...etractions-in-large-precategories.lagda.md | 69 ++++++++++++++++
 .../retractions-in-precategories.lagda.md     | 64 +++++++++++++++
 .../sections-in-categories.lagda.md           | 67 ++++++++++++++++
 .../sections-in-large-categories.lagda.md     | 78 +++++++++++++++++++
 .../sections-in-large-precategories.lagda.md  | 69 ++++++++++++++++
 .../sections-in-precategories.lagda.md        | 64 +++++++++++++++
 8 files changed, 556 insertions(+)
 create mode 100644 src/category-theory/retractions-in-categories.lagda.md
 create mode 100644 src/category-theory/retractions-in-large-categories.lagda.md
 create mode 100644 src/category-theory/retractions-in-large-precategories.lagda.md
 create mode 100644 src/category-theory/retractions-in-precategories.lagda.md
 create mode 100644 src/category-theory/sections-in-categories.lagda.md
 create mode 100644 src/category-theory/sections-in-large-categories.lagda.md
 create mode 100644 src/category-theory/sections-in-large-precategories.lagda.md
 create mode 100644 src/category-theory/sections-in-precategories.lagda.md

diff --git a/src/category-theory/retractions-in-categories.lagda.md b/src/category-theory/retractions-in-categories.lagda.md
new file mode 100644
index 0000000000..b9cd217f54
--- /dev/null
+++ b/src/category-theory/retractions-in-categories.lagda.md
@@ -0,0 +1,67 @@
+# Retractions in categories
+
+```agda
+module category-theory.retractions-in-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.retractions-in-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [category](category-theory.categories.md) `𝒞`. A {{#concept "retraction" Disambiguation="morphism in a category" Agda=retraction-hom-Category}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  g ∘ f ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a category of being a retraction
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Category l1 l2)
+  {A B : obj-Category 𝒞} (f : hom-Category 𝒞 A B)
+  where
+
+  is-retraction-hom-Category : hom-Category 𝒞 B A → UU l2
+  is-retraction-hom-Category =
+    is-retraction-hom-Precategory (precategory-Category 𝒞) f
+```
+
+### Retractions of a morphism in a category
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Category l1 l2)
+  {A B : obj-Category 𝒞} (f : hom-Category 𝒞 A B)
+  where
+
+  retraction-hom-Category : UU l2
+  retraction-hom-Category =
+    retraction-hom-Precategory (precategory-Category 𝒞) f
+
+  module _
+    (r : retraction-hom-Category)
+    where
+
+    hom-retraction-hom-Category : hom-Category 𝒞 B A
+    hom-retraction-hom-Category =
+      hom-retraction-hom-Precategory (precategory-Category 𝒞) f r
+
+    is-retraction-retraction-hom-Category :
+      is-retraction-hom-Category 𝒞 f hom-retraction-hom-Category
+    is-retraction-retraction-hom-Category =
+      is-retraction-retraction-hom-Precategory (precategory-Category 𝒞) f r
+```
diff --git a/src/category-theory/retractions-in-large-categories.lagda.md b/src/category-theory/retractions-in-large-categories.lagda.md
new file mode 100644
index 0000000000..bdf58e295c
--- /dev/null
+++ b/src/category-theory/retractions-in-large-categories.lagda.md
@@ -0,0 +1,78 @@
+# Retractions in large categories
+
+```agda
+module category-theory.retractions-in-large-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-categories
+open import category-theory.retractions-in-large-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [large category](category-theory.large-categories.md) `𝒞`. A {{#concept "retraction" Disambiguation="morphism in a large category" Agda=retraction-hom-Large-Category}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  g ∘ f ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a large category of being a retraction
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Category α β)
+  {l1 l2 : Level} {A : obj-Large-Category 𝒞 l1}
+  {B : obj-Large-Category 𝒞 l2} (f : hom-Large-Category 𝒞 A B)
+  where
+
+  is-retraction-hom-Large-Category :
+    hom-Large-Category 𝒞 B A → UU (β l1 l1)
+  is-retraction-hom-Large-Category =
+    is-retraction-hom-Large-Precategory (large-precategory-Large-Category 𝒞) f
+```
+
+### Retractions of a morphism in a large category
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Category α β)
+  {l1 l2 : Level} {A : obj-Large-Category 𝒞 l1}
+  {B : obj-Large-Category 𝒞 l2} (f : hom-Large-Category 𝒞 A B)
+  where
+
+  retraction-hom-Large-Category : UU (β l1 l1 ⊔ β l2 l1)
+  retraction-hom-Large-Category =
+    retraction-hom-Large-Precategory (large-precategory-Large-Category 𝒞) f
+
+  module _
+    (r : retraction-hom-Large-Category)
+    where
+
+    hom-retraction-hom-Large-Category : hom-Large-Category 𝒞 B A
+    hom-retraction-hom-Large-Category =
+      hom-retraction-hom-Large-Precategory
+        ( large-precategory-Large-Category 𝒞)
+        ( f)
+        ( r)
+
+    is-retraction-retraction-hom-Large-Category :
+      is-retraction-hom-Large-Category 𝒞 f
+        ( hom-retraction-hom-Large-Category)
+    is-retraction-retraction-hom-Large-Category =
+      is-retraction-retraction-hom-Large-Precategory
+        ( large-precategory-Large-Category 𝒞)
+        ( f)
+        ( r)
+```
+
diff --git a/src/category-theory/retractions-in-large-precategories.lagda.md b/src/category-theory/retractions-in-large-precategories.lagda.md
new file mode 100644
index 0000000000..f12b3b1189
--- /dev/null
+++ b/src/category-theory/retractions-in-large-precategories.lagda.md
@@ -0,0 +1,69 @@
+# Retractions in large precategories
+
+```agda
+module category-theory.retractions-in-large-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [large precategory](category-theory.large-precategories.md) `𝒞`. A {{#concept "retraction" Disambiguation="morphism in a large precategory" Agda=retraction-hom-Large-Precategory}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  g ∘ f ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a large precategory of being a retraction
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Precategory α β)
+  {l1 l2 : Level} {A : obj-Large-Precategory 𝒞 l1}
+  {B : obj-Large-Precategory 𝒞 l2} (f : hom-Large-Precategory 𝒞 A B)
+  where
+
+  is-retraction-hom-Large-Precategory :
+    hom-Large-Precategory 𝒞 B A → UU (β l1 l1)
+  is-retraction-hom-Large-Precategory g =
+    comp-hom-Large-Precategory 𝒞 g f ＝ id-hom-Large-Precategory 𝒞
+```
+
+### Retractions of a morphism in a large precategory
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Precategory α β)
+  {l1 l2 : Level} {A : obj-Large-Precategory 𝒞 l1}
+  {B : obj-Large-Precategory 𝒞 l2} (f : hom-Large-Precategory 𝒞 A B)
+  where
+
+  retraction-hom-Large-Precategory : UU (β l1 l1 ⊔ β l2 l1)
+  retraction-hom-Large-Precategory =
+    Σ (hom-Large-Precategory 𝒞 B A) (is-retraction-hom-Large-Precategory 𝒞 f)
+
+  module _
+    (r : retraction-hom-Large-Precategory)
+    where
+
+    hom-retraction-hom-Large-Precategory : hom-Large-Precategory 𝒞 B A
+    hom-retraction-hom-Large-Precategory = pr1 r
+
+    is-retraction-retraction-hom-Large-Precategory :
+      is-retraction-hom-Large-Precategory 𝒞 f
+        ( hom-retraction-hom-Large-Precategory)
+    is-retraction-retraction-hom-Large-Precategory = pr2 r
+```
+
diff --git a/src/category-theory/retractions-in-precategories.lagda.md b/src/category-theory/retractions-in-precategories.lagda.md
new file mode 100644
index 0000000000..03fe348305
--- /dev/null
+++ b/src/category-theory/retractions-in-precategories.lagda.md
@@ -0,0 +1,64 @@
+# Retractions in precategories
+
+```agda
+module category-theory.retractions-in-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [precategory](category-theory.precategories.md) `𝒞`. A {{#concept "retraction" Disambiguation="morphism in a precategory" Agda=retraction-hom-Precategory}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  g ∘ f ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a precategory of being a retraction
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Precategory l1 l2)
+  {A B : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 A B)
+  where
+
+  is-retraction-hom-Precategory : hom-Precategory 𝒞 B A → UU l2
+  is-retraction-hom-Precategory g =
+    comp-hom-Precategory 𝒞 g f ＝ id-hom-Precategory 𝒞
+```
+
+### Retractions of a morphism in a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Precategory l1 l2)
+  {A B : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 A B)
+  where
+
+  retraction-hom-Precategory : UU l2
+  retraction-hom-Precategory =
+    Σ (hom-Precategory 𝒞 B A) (is-retraction-hom-Precategory 𝒞 f)
+
+  module _
+    (r : retraction-hom-Precategory)
+    where
+
+    hom-retraction-hom-Precategory : hom-Precategory 𝒞 B A
+    hom-retraction-hom-Precategory = pr1 r
+
+    is-retraction-retraction-hom-Precategory :
+      is-retraction-hom-Precategory 𝒞 f hom-retraction-hom-Precategory
+    is-retraction-retraction-hom-Precategory = pr2 r
+```
diff --git a/src/category-theory/sections-in-categories.lagda.md b/src/category-theory/sections-in-categories.lagda.md
new file mode 100644
index 0000000000..634124663a
--- /dev/null
+++ b/src/category-theory/sections-in-categories.lagda.md
@@ -0,0 +1,67 @@
+# Sections in categories
+
+```agda
+module category-theory.sections-in-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.sections-in-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [category](category-theory.categories.md) `𝒞`. A {{#concept "section" Disambiguation="morphism in a category" Agda=section-hom-Category}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  f ∘ g ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a category of being a section
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Category l1 l2)
+  {A B : obj-Category 𝒞} (f : hom-Category 𝒞 A B)
+  where
+
+  is-section-hom-Category : hom-Category 𝒞 B A → UU l2
+  is-section-hom-Category =
+    is-section-hom-Precategory (precategory-Category 𝒞) f
+```
+
+### Sections of a morphism in a category
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Category l1 l2)
+  {A B : obj-Category 𝒞} (f : hom-Category 𝒞 A B)
+  where
+
+  section-hom-Category : UU l2
+  section-hom-Category =
+    section-hom-Precategory (precategory-Category 𝒞) f
+
+  module _
+    (r : section-hom-Category)
+    where
+
+    hom-section-hom-Category : hom-Category 𝒞 B A
+    hom-section-hom-Category =
+      hom-section-hom-Precategory (precategory-Category 𝒞) f r
+
+    is-section-section-hom-Category :
+      is-section-hom-Category 𝒞 f hom-section-hom-Category
+    is-section-section-hom-Category =
+      is-section-section-hom-Precategory (precategory-Category 𝒞) f r
+```
diff --git a/src/category-theory/sections-in-large-categories.lagda.md b/src/category-theory/sections-in-large-categories.lagda.md
new file mode 100644
index 0000000000..d278e715d5
--- /dev/null
+++ b/src/category-theory/sections-in-large-categories.lagda.md
@@ -0,0 +1,78 @@
+# Sections in large categories
+
+```agda
+module category-theory.sections-in-large-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-categories
+open import category-theory.sections-in-large-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [large category](category-theory.large-categories.md) `𝒞`. A {{#concept "section" Disambiguation="morphism in a large category" Agda=section-hom-Large-Category}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  f ∘ g ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a large category of being a section
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Category α β)
+  {l1 l2 : Level} {A : obj-Large-Category 𝒞 l1}
+  {B : obj-Large-Category 𝒞 l2} (f : hom-Large-Category 𝒞 A B)
+  where
+
+  is-section-hom-Large-Category :
+    hom-Large-Category 𝒞 B A → UU (β l2 l2)
+  is-section-hom-Large-Category =
+    is-section-hom-Large-Precategory (large-precategory-Large-Category 𝒞) f
+```
+
+### Sections of a morphism in a large category
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Category α β)
+  {l1 l2 : Level} {A : obj-Large-Category 𝒞 l1}
+  {B : obj-Large-Category 𝒞 l2} (f : hom-Large-Category 𝒞 A B)
+  where
+
+  section-hom-Large-Category : UU (β l2 l1 ⊔ β l2 l2)
+  section-hom-Large-Category =
+    section-hom-Large-Precategory (large-precategory-Large-Category 𝒞) f
+
+  module _
+    (r : section-hom-Large-Category)
+    where
+
+    hom-section-hom-Large-Category : hom-Large-Category 𝒞 B A
+    hom-section-hom-Large-Category =
+      hom-section-hom-Large-Precategory
+        ( large-precategory-Large-Category 𝒞)
+        ( f)
+        ( r)
+
+    is-section-section-hom-Large-Category :
+      is-section-hom-Large-Category 𝒞 f
+        ( hom-section-hom-Large-Category)
+    is-section-section-hom-Large-Category =
+      is-section-section-hom-Large-Precategory
+        ( large-precategory-Large-Category 𝒞)
+        ( f)
+        ( r)
+```
+
diff --git a/src/category-theory/sections-in-large-precategories.lagda.md b/src/category-theory/sections-in-large-precategories.lagda.md
new file mode 100644
index 0000000000..70199ce654
--- /dev/null
+++ b/src/category-theory/sections-in-large-precategories.lagda.md
@@ -0,0 +1,69 @@
+# Sections in large precategories
+
+```agda
+module category-theory.sections-in-large-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [large precategory](category-theory.large-precategories.md) `𝒞`. A {{#concept "section" Disambiguation="morphism in a large precategory" Agda=section-hom-Large-Precategory}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  f ∘ g ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a large precategory of being a section
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Precategory α β)
+  {l1 l2 : Level} {A : obj-Large-Precategory 𝒞 l1}
+  {B : obj-Large-Precategory 𝒞 l2} (f : hom-Large-Precategory 𝒞 A B)
+  where
+
+  is-section-hom-Large-Precategory :
+    hom-Large-Precategory 𝒞 B A → UU (β l2 l2)
+  is-section-hom-Large-Precategory g =
+    comp-hom-Large-Precategory 𝒞 f g ＝ id-hom-Large-Precategory 𝒞
+```
+
+### Sections of a morphism in a large precategory
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Precategory α β)
+  {l1 l2 : Level} {A : obj-Large-Precategory 𝒞 l1}
+  {B : obj-Large-Precategory 𝒞 l2} (f : hom-Large-Precategory 𝒞 A B)
+  where
+
+  section-hom-Large-Precategory : UU (β l2 l1 ⊔ β l2 l2)
+  section-hom-Large-Precategory =
+    Σ (hom-Large-Precategory 𝒞 B A) (is-section-hom-Large-Precategory 𝒞 f)
+
+  module _
+    (r : section-hom-Large-Precategory)
+    where
+
+    hom-section-hom-Large-Precategory : hom-Large-Precategory 𝒞 B A
+    hom-section-hom-Large-Precategory = pr1 r
+
+    is-section-section-hom-Large-Precategory :
+      is-section-hom-Large-Precategory 𝒞 f
+        ( hom-section-hom-Large-Precategory)
+    is-section-section-hom-Large-Precategory = pr2 r
+```
+
diff --git a/src/category-theory/sections-in-precategories.lagda.md b/src/category-theory/sections-in-precategories.lagda.md
new file mode 100644
index 0000000000..d40d3e8a8f
--- /dev/null
+++ b/src/category-theory/sections-in-precategories.lagda.md
@@ -0,0 +1,64 @@
+# Sections in precategories
+
+```agda
+module category-theory.sections-in-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [precategory](category-theory.precategories.md) `𝒞`. A {{#concept "section" Disambiguation="morphism in a precategory" Agda=section-hom-Precategory}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  f ∘ g ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a precategory of being a section
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Precategory l1 l2)
+  {A B : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 A B)
+  where
+
+  is-section-hom-Precategory : hom-Precategory 𝒞 B A → UU l2
+  is-section-hom-Precategory g =
+    comp-hom-Precategory 𝒞 f g ＝ id-hom-Precategory 𝒞
+```
+
+### Sections of a morphism in a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Precategory l1 l2)
+  {A B : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 A B)
+  where
+
+  section-hom-Precategory : UU l2
+  section-hom-Precategory =
+    Σ (hom-Precategory 𝒞 B A) (is-section-hom-Precategory 𝒞 f)
+
+  module _
+    (s : section-hom-Precategory)
+    where
+
+    hom-section-hom-Precategory : hom-Precategory 𝒞 B A
+    hom-section-hom-Precategory = pr1 s
+
+    is-section-section-hom-Precategory :
+      is-section-hom-Precategory 𝒞 f hom-section-hom-Precategory
+    is-section-section-hom-Precategory = pr2 s
+```

From ef23fbceb4fc4314d62dec8b3682261812b16cda Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Mar 2024 17:46:22 +0100
Subject: [PATCH 2/2] work

---
 ...rtible-morphisms-in-precategories.lagda.md | 1046 +++++++++++++++++
 .../isomorphisms-in-precategories.lagda.md    |  135 ++-
 2 files changed, 1147 insertions(+), 34 deletions(-)
 create mode 100644 src/category-theory/invertible-morphisms-in-precategories.lagda.md

diff --git a/src/category-theory/invertible-morphisms-in-precategories.lagda.md b/src/category-theory/invertible-morphisms-in-precategories.lagda.md
new file mode 100644
index 0000000000..b84f212252
--- /dev/null
+++ b/src/category-theory/invertible-morphisms-in-precategories.lagda.md
@@ -0,0 +1,1046 @@
+# Invertible Morphisms in precategories
+
+```agda
+module category-theory.invertible-morphisms-in-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.precategories
+open import category-theory.retractions-in-precategories
+open import category-theory.sections-in-precategories
+
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A morphism `f : x → y` in a [precategory](category-theory.precategories.md) `C` is said to be
+{{#concept "invertible" Disambiguation="morphism in a precategory" Agda=is-invertible-hom-Precategory}}
+if there is a morphism `g : y → x` which is both a [section](category-theory.sections-in-precategories.md) of `f` and a [retraction](category-theory.retractions-in-precategories.md) of `f`. In other words, `f` is invertible if there is a morphism `g` equipped with [identifications](foundation-core.identity-types.md) `f ∘ g ＝ id` and `g ∘ f ＝ id`.
+
+## Definitions
+
+### The predicate of being an inverse of a morphism in a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} {f : hom-Precategory C x y}
+  where
+
+  is-inverse-hom-Precategory : (g : hom-Precategory C y x) → UU l2
+  is-inverse-hom-Precategory g =
+    is-section-hom-Precategory C f g × is-retraction-hom-Precategory C f g
+```
+
+### The predicate of being an invertible morphism in a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} (f : hom-Precategory C x y)
+  where
+
+  is-invertible-hom-Precategory : UU l2
+  is-invertible-hom-Precategory =
+    Σ ( hom-Precategory C y x)
+      ( λ g →
+        ( is-section-hom-Precategory C f g) ×
+        ( is-retraction-hom-Precategory C f g))
+
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} {f : hom-Precategory C x y}
+  (H : is-invertible-hom-Precategory C f)
+  where
+
+  hom-inv-is-invertible-hom-Precategory : hom-Precategory C y x
+  hom-inv-is-invertible-hom-Precategory = pr1 H
+
+  is-section-hom-inv-is-invertible-hom-Precategory :
+    is-section-hom-Precategory C f hom-inv-is-invertible-hom-Precategory
+  is-section-hom-inv-is-invertible-hom-Precategory = pr1 (pr2 H)
+
+  section-is-invertible-hom-Precategory :
+    section-hom-Precategory C f
+  pr1 section-is-invertible-hom-Precategory =
+    hom-inv-is-invertible-hom-Precategory
+  pr2 section-is-invertible-hom-Precategory =
+    is-section-hom-inv-is-invertible-hom-Precategory
+
+  is-retraction-hom-inv-is-invertible-hom-Precategory :
+    is-retraction-hom-Precategory C f hom-inv-is-invertible-hom-Precategory
+  is-retraction-hom-inv-is-invertible-hom-Precategory = pr2 (pr2 H)
+
+  retraction-is-invertible-hom-Precategory :
+    retraction-hom-Precategory C f
+  pr1 retraction-is-invertible-hom-Precategory =
+    hom-inv-is-invertible-hom-Precategory
+  pr2 retraction-is-invertible-hom-Precategory =
+    is-retraction-hom-inv-is-invertible-hom-Precategory
+
+  is-inverse-hom-inv-is-invertible-hom-Precategory :
+    is-inverse-hom-Precategory C hom-inv-is-invertible-hom-Precategory
+  pr1 is-inverse-hom-inv-is-invertible-hom-Precategory =
+    is-section-hom-inv-is-invertible-hom-Precategory
+  pr2 is-inverse-hom-inv-is-invertible-hom-Precategory =
+    is-retraction-hom-inv-is-invertible-hom-Precategory
+```
+
+### Invertible morphisms in a precategory
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  (x y : obj-Precategory C)
+  where
+
+  invertible-hom-Precategory : UU l2
+  invertible-hom-Precategory =
+    Σ (hom-Precategory C x y) (is-invertible-hom-Precategory C)
+
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  (f : invertible-hom-Precategory C x y)
+  where
+
+  hom-invertible-hom-Precategory : hom-Precategory C x y
+  hom-invertible-hom-Precategory = pr1 f
+
+  is-invertible-hom-iso-Precategory :
+    is-invertible-hom-Precategory C hom-invertible-hom-Precategory
+  is-invertible-hom-iso-Precategory = pr2 f
+
+  hom-inv-invertible-hom-Precategory : hom-Precategory C y x
+  hom-inv-invertible-hom-Precategory =
+    hom-inv-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory)
+
+  is-section-hom-inv-invertible-hom-Precategory :
+    is-section-hom-Precategory C
+      ( hom-invertible-hom-Precategory)
+      ( hom-inv-invertible-hom-Precategory)
+  is-section-hom-inv-invertible-hom-Precategory =
+    is-section-hom-inv-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory)
+
+  is-retraction-hom-inv-invertible-hom-Precategory :
+    is-retraction-hom-Precategory C
+      ( hom-invertible-hom-Precategory)
+      ( hom-inv-invertible-hom-Precategory)
+  is-retraction-hom-inv-invertible-hom-Precategory =
+    is-retraction-hom-inv-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory)
+```
+
+## Examples
+
+### The invertible identity morphisms
+
+For any object `x` of a precategory `C`, the identity morphism `id : hom x x` is an invertible morphism
+from `x` to `x` since `id ∘ id = id`, i.e., the identity morphism is its own inverse.
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) {x : obj-Precategory C}
+  where
+
+  is-invertible-hom-id-hom-Precategory :
+    is-invertible-hom-Precategory C (id-hom-Precategory C {x})
+  pr1 is-invertible-hom-id-hom-Precategory = id-hom-Precategory C
+  pr1 (pr2 is-invertible-hom-id-hom-Precategory) =
+    left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
+  pr2 (pr2 is-invertible-hom-id-hom-Precategory) =
+    right-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
+
+  id-invertible-hom-Precategory : invertible-hom-Precategory C x x
+  pr1 id-invertible-hom-Precategory = id-hom-Precategory C
+  pr2 id-invertible-hom-Precategory = is-invertible-hom-id-hom-Precategory
+```
+
+### Identifications induce invertible morphisms
+
+For any two objects `x` and `y` of a precategory `C`, there a map
+
+```text
+  x ＝ y → invertible-hom-Precategory C x y.
+```
+
+We construct this map by observing that we already have a map
+
+```text
+  hom-eq-Precategory : x ＝ y → hom-Precategory C x y
+```
+
+satisfying `hom-eq-Precategory refl ≐ id-hom-Precategory`. Since the identity morphism is invertible, it follows by identification elimination that all morphisms of the form `hom-eq-Precategory p` are invertible.
+
+Note that we could have defined the map
+
+```text
+  invertible-hom-eq-Precategory : x ＝ y → invertible-hom-Precategory C x y.
+```
+
+directly by identification elimination. However, with our current definition it follows that the underlying map of `invertible-hom-eq-Precategory p` always computes to `hom-eq-Precategory p`, which could sometimes be useful to know.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  where
+
+  invertible-hom-eq-Precategory :
+    (x y : obj-Precategory C) → x ＝ y → invertible-hom-Precategory C x y
+  pr1 (invertible-hom-eq-Precategory x y p) =
+    hom-eq-Precategory C x y p
+  pr2 (invertible-hom-eq-Precategory x .x refl) =
+    is-invertible-hom-id-hom-Precategory C
+
+  compute-hom-invertible-hom-eq-Precategory :
+    {x y : obj-Precategory C} (p : x ＝ y) →
+    hom-eq-Precategory C x y p ＝
+    hom-invertible-hom-Precategory C (invertible-hom-eq-Precategory x y p)
+  compute-hom-invertible-hom-eq-Precategory p = refl
+```
+
+## Properties
+
+### Being an invertible morphism is a proposition
+
+Let `f : hom x y` and suppose `g g' : hom y x` are both inverses of `f`.
+It is enough to show that `g = g'` since being a section and being a retraction
+is always a [proposition](foundation-core.propositions.md).
+Using that `g` and `g'` are both inverses of `f` we have the following chain of identifications:
+
+```text
+  g ＝ g ∘ id
+    ＝ g ∘ (f ∘ g')
+    ＝ (g ∘ f) ∘ g'
+    ＝ id ∘ g'
+    ＝ g'.
+```
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  where
+
+  all-elements-equal-is-invertible-hom-Precategory :
+    (f : hom-Precategory C x y)
+    (H K : is-invertible-hom-Precategory C f) → H ＝ K
+  all-elements-equal-is-invertible-hom-Precategory f
+    (g , p , q) (g' , p' , q') =
+    eq-type-subtype
+      ( λ g →
+        product-Prop
+          ( Id-Prop
+            ( hom-set-Precategory C y y)
+            ( comp-hom-Precategory C f g)
+            ( id-hom-Precategory C))
+          ( Id-Prop
+            ( hom-set-Precategory C x x)
+            ( comp-hom-Precategory C g f)
+            ( id-hom-Precategory C)))
+      ( ( inv (right-unit-law-comp-hom-Precategory C g)) ∙
+        ( ap ( comp-hom-Precategory C g) (inv p')) ∙
+        ( inv (associative-comp-hom-Precategory C g f g')) ∙
+        ( ap ( comp-hom-Precategory' C g') q) ∙
+        ( left-unit-law-comp-hom-Precategory C g'))
+
+  is-prop-is-invertible-hom-Precategory :
+    (f : hom-Precategory C x y) →
+    is-prop (is-invertible-hom-Precategory C f)
+  is-prop-is-invertible-hom-Precategory f =
+    is-prop-all-elements-equal
+      ( all-elements-equal-is-invertible-hom-Precategory f)
+
+  is-invertible-hom-prop-Precategory :
+    (f : hom-Precategory C x y) → Prop l2
+  pr1 (is-invertible-hom-prop-Precategory f) =
+    is-invertible-hom-Precategory C f
+  pr2 (is-invertible-hom-prop-Precategory f) =
+    is-prop-is-invertible-hom-Precategory f
+```
+
+### Equality of invertible morphism is equality of their underlying morphisms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  where
+
+  eq-invertible-hom-eq-hom-Precategory :
+    (f g : invertible-hom-Precategory C x y) →
+    hom-invertible-hom-Precategory C f ＝ hom-invertible-hom-Precategory C g →
+    f ＝ g
+  eq-invertible-hom-eq-hom-Precategory f g =
+    eq-type-subtype (is-invertible-hom-prop-Precategory C)
+```
+
+### The type of invertible morphisms form a set
+
+The type of invertible morphisms between objects `x y : A` is a
+[subtype](foundation-core.subtypes.md) of the [foundation-core.sets.md)
+`hom x y` since being an invertible morphism is a proposition.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  where
+
+  is-set-invertible-hom-Precategory : is-set (invertible-hom-Precategory C x y)
+  is-set-invertible-hom-Precategory =
+    is-set-type-subtype
+      ( is-invertible-hom-prop-Precategory C)
+      ( is-set-hom-Precategory C x y)
+
+  invertible-hom-set-Precategory : Set l2
+  pr1 invertible-hom-set-Precategory = invertible-hom-Precategory C x y
+  pr2 invertible-hom-set-Precategory = is-set-invertible-hom-Precategory
+```
+
+### Invertible morphisms are closed under composition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y z : obj-Precategory C}
+  {g : hom-Precategory C y z}
+  {f : hom-Precategory C x y}
+  where
+
+  hom-comp-is-invertible-hom-Precategory :
+    is-invertible-hom-Precategory C g →
+    is-invertible-hom-Precategory C f →
+    hom-Precategory C z x
+  hom-comp-is-invertible-hom-Precategory q p =
+    comp-hom-Precategory C
+      ( hom-inv-is-invertible-hom-Precategory C p)
+      ( hom-inv-is-invertible-hom-Precategory C q)
+
+  is-section-comp-is-invertible-hom-Precategory :
+    (q : is-invertible-hom-Precategory C g)
+    (p : is-invertible-hom-Precategory C f) →
+    comp-hom-Precategory C
+      ( comp-hom-Precategory C g f)
+      ( hom-comp-is-invertible-hom-Precategory q p) ＝
+    id-hom-Precategory C
+  is-section-comp-is-invertible-hom-Precategory q p =
+    ( associative-comp-hom-Precategory C g f _) ∙
+    ( ap
+      ( comp-hom-Precategory C g)
+      ( ( inv
+          ( associative-comp-hom-Precategory C f
+            ( hom-inv-is-invertible-hom-Precategory C p)
+            ( hom-inv-is-invertible-hom-Precategory C q))) ∙
+        ( ap
+          ( λ h →
+            comp-hom-Precategory C h
+              ( hom-inv-is-invertible-hom-Precategory C q))
+          ( is-section-hom-inv-is-invertible-hom-Precategory C p) ∙
+          ( left-unit-law-comp-hom-Precategory C
+            ( hom-inv-is-invertible-hom-Precategory C q))))) ∙
+    ( is-section-hom-inv-is-invertible-hom-Precategory C q)
+
+  is-retraction-comp-is-invertible-hom-Precategory :
+    (q : is-invertible-hom-Precategory C g)
+    (p : is-invertible-hom-Precategory C f) →
+    ( comp-hom-Precategory C
+      ( hom-comp-is-invertible-hom-Precategory q p)
+      ( comp-hom-Precategory C g f)) ＝
+    ( id-hom-Precategory C)
+  is-retraction-comp-is-invertible-hom-Precategory q p =
+    ( associative-comp-hom-Precategory C
+      ( hom-inv-is-invertible-hom-Precategory C p)
+      ( hom-inv-is-invertible-hom-Precategory C q)
+      ( comp-hom-Precategory C g f)) ∙
+    ( ap
+      ( comp-hom-Precategory
+        ( C)
+        ( hom-inv-is-invertible-hom-Precategory C p))
+      ( ( inv
+          ( associative-comp-hom-Precategory C
+            ( hom-inv-is-invertible-hom-Precategory C q)
+            ( g)
+            ( f))) ∙
+        ( ap
+            ( λ h → comp-hom-Precategory C h f)
+            ( is-retraction-hom-inv-is-invertible-hom-Precategory C q)) ∙
+        ( left-unit-law-comp-hom-Precategory C f))) ∙
+    ( is-retraction-hom-inv-is-invertible-hom-Precategory C p)
+
+  is-invertible-hom-comp-is-invertible-hom-Precategory :
+    is-invertible-hom-Precategory C g → is-invertible-hom-Precategory C f →
+    is-invertible-hom-Precategory C (comp-hom-Precategory C g f)
+  pr1 (is-invertible-hom-comp-is-invertible-hom-Precategory q p) =
+    hom-comp-is-invertible-hom-Precategory q p
+  pr1 (pr2 (is-invertible-hom-comp-is-invertible-hom-Precategory q p)) =
+    is-section-comp-is-invertible-hom-Precategory q p
+  pr2 (pr2 (is-invertible-hom-comp-is-invertible-hom-Precategory q p)) =
+    is-retraction-comp-is-invertible-hom-Precategory q p
+```
+
+### The composition operation on invertible morphisms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y z : obj-Precategory C}
+  (g : invertible-hom-Precategory C y z)
+  (f : invertible-hom-Precategory C x y)
+  where
+
+  hom-comp-invertible-hom-Precategory :
+    hom-Precategory C x z
+  hom-comp-invertible-hom-Precategory =
+    comp-hom-Precategory C
+      ( hom-invertible-hom-Precategory C g)
+      ( hom-invertible-hom-Precategory C f)
+
+  is-invertible-hom-comp-invertible-hom-Precategory :
+    is-invertible-hom-Precategory C hom-comp-invertible-hom-Precategory
+  is-invertible-hom-comp-invertible-hom-Precategory =
+    is-invertible-hom-comp-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory C g)
+      ( is-invertible-hom-iso-Precategory C f)
+
+  comp-invertible-hom-Precategory : invertible-hom-Precategory C x z
+  pr1 comp-invertible-hom-Precategory =
+    hom-comp-invertible-hom-Precategory
+  pr2 comp-invertible-hom-Precategory =
+    is-invertible-hom-comp-invertible-hom-Precategory
+
+  hom-inv-comp-invertible-hom-Precategory : hom-Precategory C z x
+  hom-inv-comp-invertible-hom-Precategory =
+    hom-inv-invertible-hom-Precategory C comp-invertible-hom-Precategory
+
+  is-section-inv-comp-invertible-hom-Precategory :
+    ( comp-hom-Precategory C
+      ( hom-comp-invertible-hom-Precategory)
+      ( hom-inv-comp-invertible-hom-Precategory)) ＝
+    ( id-hom-Precategory C)
+  is-section-inv-comp-invertible-hom-Precategory =
+    is-section-hom-inv-invertible-hom-Precategory C
+      ( comp-invertible-hom-Precategory)
+
+  is-retraction-inv-comp-invertible-hom-Precategory :
+    ( comp-hom-Precategory C
+      ( hom-inv-comp-invertible-hom-Precategory)
+      ( hom-comp-invertible-hom-Precategory)) ＝
+    ( id-hom-Precategory C)
+  is-retraction-inv-comp-invertible-hom-Precategory =
+    is-retraction-hom-inv-invertible-hom-Precategory C
+      ( comp-invertible-hom-Precategory)
+```
+
+### Inverses of invertible morphisms are invertible morphisms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  {f : hom-Precategory C x y}
+  where
+
+  is-invertible-hom-inv-is-invertible-hom-Precategory :
+    (p : is-invertible-hom-Precategory C f) →
+    is-invertible-hom-Precategory C
+      ( hom-inv-invertible-hom-Precategory C (f , p))
+  pr1 (is-invertible-hom-inv-is-invertible-hom-Precategory p) = f
+  pr1 (pr2 (is-invertible-hom-inv-is-invertible-hom-Precategory p)) =
+    is-retraction-hom-inv-is-invertible-hom-Precategory C p
+  pr2 (pr2 (is-invertible-hom-inv-is-invertible-hom-Precategory p)) =
+    is-section-hom-inv-is-invertible-hom-Precategory C p
+```
+
+### Inverses of invertible morphisms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  where
+
+  inv-invertible-hom-Precategory :
+    invertible-hom-Precategory C x y → invertible-hom-Precategory C y x
+  pr1 (inv-invertible-hom-Precategory f) =
+    hom-inv-invertible-hom-Precategory C f
+  pr2 (inv-invertible-hom-Precategory f) =
+    is-invertible-hom-inv-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory C f)
+
+  is-invertible-hom-inv-invertible-hom-Precategory :
+    (f : invertible-hom-Precategory C x y) →
+    is-invertible-hom-Precategory C (hom-inv-invertible-hom-Precategory C f)
+  is-invertible-hom-inv-invertible-hom-Precategory f =
+    is-invertible-hom-iso-Precategory C (inv-invertible-hom-Precategory f)
+```
+
+### Groupoid laws of invertible morphisms in precategories
+
+#### Composition of invertible morphisms satisfies the unit laws
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  (f : invertible-hom-Precategory C x y)
+  where
+
+  left-unit-law-comp-invertible-hom-Precategory :
+    comp-invertible-hom-Precategory C (id-invertible-hom-Precategory C) f ＝ f
+  left-unit-law-comp-invertible-hom-Precategory =
+    eq-invertible-hom-eq-hom-Precategory C
+      ( comp-invertible-hom-Precategory C (id-invertible-hom-Precategory C) f)
+      ( f)
+      ( left-unit-law-comp-hom-Precategory C
+        ( hom-invertible-hom-Precategory C f))
+
+  right-unit-law-comp-invertible-hom-Precategory :
+    comp-invertible-hom-Precategory C f (id-invertible-hom-Precategory C) ＝ f
+  right-unit-law-comp-invertible-hom-Precategory =
+    eq-invertible-hom-eq-hom-Precategory C
+      ( comp-invertible-hom-Precategory C f (id-invertible-hom-Precategory C))
+      ( f)
+      ( right-unit-law-comp-hom-Precategory C
+        ( hom-invertible-hom-Precategory C f))
+```
+
+#### Composition of invertible morphisms is associative
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y z w : obj-Precategory C}
+  (h : invertible-hom-Precategory C z w)
+  (g : invertible-hom-Precategory C y z)
+  (f : invertible-hom-Precategory C x y)
+  where
+
+  associative-comp-invertible-hom-Precategory :
+    ( comp-invertible-hom-Precategory C
+      ( comp-invertible-hom-Precategory C h g)
+      ( f)) ＝
+    ( comp-invertible-hom-Precategory C
+      ( h)
+      ( comp-invertible-hom-Precategory C g f))
+  associative-comp-invertible-hom-Precategory =
+    eq-invertible-hom-eq-hom-Precategory C
+      ( comp-invertible-hom-Precategory C
+        ( comp-invertible-hom-Precategory C h g)
+        ( f))
+      ( comp-invertible-hom-Precategory C
+        ( h)
+        ( comp-invertible-hom-Precategory C g f))
+      ( associative-comp-hom-Precategory C
+        ( hom-invertible-hom-Precategory C h)
+        ( hom-invertible-hom-Precategory C g)
+        ( hom-invertible-hom-Precategory C f))
+```
+
+#### Composition of invertible morphisms satisfies inverse laws
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  (f : invertible-hom-Precategory C x y)
+  where
+
+  left-inverse-law-comp-invertible-hom-Precategory :
+    ( comp-invertible-hom-Precategory C
+      ( inv-invertible-hom-Precategory C f)
+      ( f)) ＝
+    ( id-invertible-hom-Precategory C)
+  left-inverse-law-comp-invertible-hom-Precategory =
+    eq-invertible-hom-eq-hom-Precategory C
+      ( comp-invertible-hom-Precategory C
+        ( inv-invertible-hom-Precategory C f)
+        ( f))
+      ( id-invertible-hom-Precategory C)
+      ( is-retraction-hom-inv-invertible-hom-Precategory C f)
+
+  right-inverse-law-comp-invertible-hom-Precategory :
+    ( comp-invertible-hom-Precategory C
+      ( f)
+      ( inv-invertible-hom-Precategory C f)) ＝
+    ( id-invertible-hom-Precategory C)
+  right-inverse-law-comp-invertible-hom-Precategory =
+    eq-invertible-hom-eq-hom-Precategory C
+      ( comp-invertible-hom-Precategory C f
+        ( inv-invertible-hom-Precategory C f))
+      ( id-invertible-hom-Precategory C)
+      ( is-section-hom-inv-invertible-hom-Precategory C f)
+```
+
+### The inverse operation is a fibered involution on invertible morphisms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  where
+
+  is-fibered-involution-inv-invertible-hom-Precategory :
+    {x y : obj-Precategory C} →
+    inv-invertible-hom-Precategory C {y} {x} ∘
+    inv-invertible-hom-Precategory C {x} {y} ~
+    id
+  is-fibered-involution-inv-invertible-hom-Precategory f = refl
+
+  is-equiv-inv-invertible-hom-Precategory :
+    {x y : obj-Precategory C} →
+    is-equiv (inv-invertible-hom-Precategory C {x} {y})
+  is-equiv-inv-invertible-hom-Precategory =
+    is-equiv-is-invertible
+      ( inv-invertible-hom-Precategory C)
+      ( is-fibered-involution-inv-invertible-hom-Precategory)
+      ( is-fibered-involution-inv-invertible-hom-Precategory)
+
+  equiv-inv-invertible-hom-Precategory :
+    {x y : obj-Precategory C} →
+    invertible-hom-Precategory C x y ≃ invertible-hom-Precategory C y x
+  pr1 equiv-inv-invertible-hom-Precategory =
+    inv-invertible-hom-Precategory C
+  pr2 equiv-inv-invertible-hom-Precategory =
+    is-equiv-inv-invertible-hom-Precategory
+```
+
+### A morphism `f` is invertible if and only if precomposition by `f` is an equivalence
+
+**Proof:** If `f` is invertible with inverse `f⁻¹`, then precomposing with
+`f⁻¹` is an inverse of precomposing with `f`. The only interesting direction is
+therefore the converse.
+
+Suppose that precomposing with `f` is an equivalence, for any object `z`. Then
+
+```text
+  - ∘ f : hom y x → hom x x
+```
+
+is an equivalence. In particular, there is a unique morphism `g : y → x` such
+that `g ∘ f ＝ id`. Thus we have a retraction of `f`. To see that `g` is also a
+section, note that the map
+
+```text
+  - ∘ f : hom y y → hom x y
+```
+
+is an equivalence. In particular, it is injective. Therefore it suffices to show
+that `(f ∘ g) ∘ f ＝ id ∘ f`. To see this, we calculate
+
+```text
+  (f ∘ g) ∘ f ＝ f ∘ (g ∘ f) ＝ f ∘ id ＝ f ＝ id ∘ f.
+```
+
+This completes the proof.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  {f : hom-Precategory C x y}
+  (H : (z : obj-Precategory C) → is-equiv (precomp-hom-Precategory C f z))
+  where
+
+  hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory :
+    hom-Precategory C y x
+  hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory =
+    map-inv-is-equiv (H x) (id-hom-Precategory C)
+
+  is-retraction-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory :
+    is-retraction-hom-Precategory C f
+      ( hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory)
+  is-retraction-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory =
+    is-section-map-inv-is-equiv (H x) (id-hom-Precategory C)
+
+  is-section-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory :
+    is-section-hom-Precategory C f
+      ( hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory)
+  is-section-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory =
+    is-injective-is-equiv
+      ( H y)
+      ( ( associative-comp-hom-Precategory C
+          ( f)
+          ( hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory)
+          ( f)) ∙
+        ( ap
+          ( comp-hom-Precategory C f)
+          ( is-retraction-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory)) ∙
+        ( right-unit-law-comp-hom-Precategory C f) ∙
+        ( inv (left-unit-law-comp-hom-Precategory C f)))
+
+  is-invertible-hom-is-equiv-precomp-hom-Precategory :
+    is-invertible-hom-Precategory C f
+  pr1 is-invertible-hom-is-equiv-precomp-hom-Precategory =
+    hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory
+  pr1 (pr2 is-invertible-hom-is-equiv-precomp-hom-Precategory) =
+    is-section-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory
+  pr2 (pr2 is-invertible-hom-is-equiv-precomp-hom-Precategory) =
+    is-retraction-hom-inv-is-invertible-hom-is-equiv-precomp-hom-Precategory
+
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  {f : hom-Precategory C x y}
+  (is-invertible-hom-f : is-invertible-hom-Precategory C f)
+  (z : obj-Precategory C)
+  where
+
+  map-inv-precomp-hom-is-invertible-hom-Precategory :
+    hom-Precategory C x z → hom-Precategory C y z
+  map-inv-precomp-hom-is-invertible-hom-Precategory =
+    precomp-hom-Precategory C
+      ( hom-inv-is-invertible-hom-Precategory C is-invertible-hom-f)
+      ( z)
+
+  is-section-map-inv-precomp-hom-is-invertible-hom-Precategory :
+    is-section
+      ( precomp-hom-Precategory C f z)
+      ( map-inv-precomp-hom-is-invertible-hom-Precategory)
+  is-section-map-inv-precomp-hom-is-invertible-hom-Precategory g =
+    ( associative-comp-hom-Precategory C
+      ( g)
+      ( hom-inv-is-invertible-hom-Precategory C is-invertible-hom-f)
+      ( f)) ∙
+    ( ap
+      ( comp-hom-Precategory C g)
+      ( is-retraction-hom-inv-is-invertible-hom-Precategory C
+        ( is-invertible-hom-f))) ∙
+    ( right-unit-law-comp-hom-Precategory C g)
+
+  is-retraction-map-inv-precomp-hom-is-invertible-hom-Precategory :
+    is-retraction
+      ( precomp-hom-Precategory C f z)
+      ( map-inv-precomp-hom-is-invertible-hom-Precategory)
+  is-retraction-map-inv-precomp-hom-is-invertible-hom-Precategory g =
+    ( associative-comp-hom-Precategory C
+      ( g)
+      ( f)
+      ( hom-inv-is-invertible-hom-Precategory C is-invertible-hom-f)) ∙
+    ( ap
+      ( comp-hom-Precategory C g)
+      ( is-section-hom-inv-is-invertible-hom-Precategory C
+        ( is-invertible-hom-f))) ∙
+    ( right-unit-law-comp-hom-Precategory C g)
+
+  is-equiv-precomp-hom-is-invertible-hom-Precategory :
+    is-equiv (precomp-hom-Precategory C f z)
+  is-equiv-precomp-hom-is-invertible-hom-Precategory =
+    is-equiv-is-invertible
+      ( map-inv-precomp-hom-is-invertible-hom-Precategory)
+      ( is-section-map-inv-precomp-hom-is-invertible-hom-Precategory)
+      ( is-retraction-map-inv-precomp-hom-is-invertible-hom-Precategory)
+
+  equiv-precomp-hom-is-invertible-hom-Precategory :
+    hom-Precategory C y z ≃ hom-Precategory C x z
+  pr1 equiv-precomp-hom-is-invertible-hom-Precategory =
+    precomp-hom-Precategory C f z
+  pr2 equiv-precomp-hom-is-invertible-hom-Precategory =
+    is-equiv-precomp-hom-is-invertible-hom-Precategory
+
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  (f : invertible-hom-Precategory C x y)
+  (z : obj-Precategory C)
+  where
+
+  is-equiv-precomp-hom-invertible-hom-Precategory :
+    is-equiv (precomp-hom-Precategory C (hom-invertible-hom-Precategory C f) z)
+  is-equiv-precomp-hom-invertible-hom-Precategory =
+    is-equiv-precomp-hom-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory C f)
+      ( z)
+
+  equiv-precomp-hom-invertible-hom-Precategory :
+    hom-Precategory C y z ≃ hom-Precategory C x z
+  equiv-precomp-hom-invertible-hom-Precategory =
+    equiv-precomp-hom-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory C f)
+      ( z)
+```
+
+### A morphism `f` is invertible if and only if postcomposition by `f` is an equivalence
+
+**Proof:** If `f` is invertible with inverse `f⁻¹`, then postcomposing with
+`f⁻¹` is an inverse of postcomposing with `f`. The only interesting direction is
+therefore the converse.
+
+Suppose that postcomposing with `f` is an equivalence, for any object `z`. Then
+
+```text
+  f ∘ - : hom y x → hom y y
+```
+
+is an equivalence. In particular, there is a unique morphism `g : y → x` such
+that `f ∘ g ＝ id`. Thus we have a section of `f`. To see that `g` is also a
+retraction, note that the map
+
+```text
+  f ∘ - : hom x x → hom x y
+```
+
+is an equivalence. In particular, it is injective. Therefore it suffices to show
+that `f ∘ (g ∘ f) ＝ f ∘ id`. To see this, we calculate
+
+```text
+  f ∘ (g ∘ f) ＝ (f ∘ g) ∘ f ＝ id ∘ f ＝ f ＝ f ∘ id.
+```
+
+This completes the proof.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  {f : hom-Precategory C x y}
+  (H : (z : obj-Precategory C) → is-equiv (postcomp-hom-Precategory C f z))
+  where
+
+  hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory :
+    hom-Precategory C y x
+  hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory =
+    map-inv-is-equiv (H y) (id-hom-Precategory C)
+
+  is-section-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory :
+    is-section-hom-Precategory C f
+      ( hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory)
+  is-section-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory =
+    is-section-map-inv-is-equiv (H y) (id-hom-Precategory C)
+
+  is-retraction-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory :
+    is-retraction-hom-Precategory C f
+      ( hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory)
+  is-retraction-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory =
+    is-injective-is-equiv
+      ( H x)
+      ( ( inv
+          ( associative-comp-hom-Precategory C
+            ( f)
+            ( hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory)
+            ( f))) ∙
+        ( ap
+          ( comp-hom-Precategory' C f)
+          ( is-section-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory)) ∙
+        ( left-unit-law-comp-hom-Precategory C f) ∙
+        ( inv (right-unit-law-comp-hom-Precategory C f)))
+
+  is-invertible-hom-is-equiv-postcomp-hom-Precategory :
+    is-invertible-hom-Precategory C f
+  pr1 is-invertible-hom-is-equiv-postcomp-hom-Precategory =
+    hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory
+  pr1 (pr2 is-invertible-hom-is-equiv-postcomp-hom-Precategory) =
+    is-section-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory
+  pr2 (pr2 is-invertible-hom-is-equiv-postcomp-hom-Precategory) =
+    is-retraction-hom-inv-is-invertible-hom-is-equiv-postcomp-hom-Precategory
+
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  {f : hom-Precategory C x y}
+  (is-invertible-hom-f : is-invertible-hom-Precategory C f)
+  (z : obj-Precategory C)
+  where
+
+  map-inv-postcomp-hom-is-invertible-hom-Precategory :
+    hom-Precategory C z y → hom-Precategory C z x
+  map-inv-postcomp-hom-is-invertible-hom-Precategory =
+    postcomp-hom-Precategory C
+      ( hom-inv-is-invertible-hom-Precategory C is-invertible-hom-f)
+      ( z)
+
+  is-section-map-inv-postcomp-hom-is-invertible-hom-Precategory :
+    is-section
+      ( postcomp-hom-Precategory C f z)
+      ( map-inv-postcomp-hom-is-invertible-hom-Precategory)
+  is-section-map-inv-postcomp-hom-is-invertible-hom-Precategory g =
+    ( inv
+      ( associative-comp-hom-Precategory C
+        ( f)
+        ( hom-inv-is-invertible-hom-Precategory C is-invertible-hom-f)
+        ( g))) ∙
+    ( ap
+      ( comp-hom-Precategory' C g)
+      ( is-section-hom-inv-is-invertible-hom-Precategory C
+        ( is-invertible-hom-f))) ∙
+    ( left-unit-law-comp-hom-Precategory C g)
+
+  is-retraction-map-inv-postcomp-hom-is-invertible-hom-Precategory :
+    is-retraction
+      ( postcomp-hom-Precategory C f z)
+      ( map-inv-postcomp-hom-is-invertible-hom-Precategory)
+  is-retraction-map-inv-postcomp-hom-is-invertible-hom-Precategory g =
+    ( inv
+      ( associative-comp-hom-Precategory C
+        ( hom-inv-is-invertible-hom-Precategory C is-invertible-hom-f)
+        ( f)
+        ( g))) ∙
+    ( ap
+      ( comp-hom-Precategory' C g)
+      ( is-retraction-hom-inv-is-invertible-hom-Precategory C
+        ( is-invertible-hom-f))) ∙
+    ( left-unit-law-comp-hom-Precategory C g)
+
+  is-equiv-postcomp-hom-is-invertible-hom-Precategory :
+    is-equiv (postcomp-hom-Precategory C f z)
+  is-equiv-postcomp-hom-is-invertible-hom-Precategory =
+    is-equiv-is-invertible
+      ( map-inv-postcomp-hom-is-invertible-hom-Precategory)
+      ( is-section-map-inv-postcomp-hom-is-invertible-hom-Precategory)
+      ( is-retraction-map-inv-postcomp-hom-is-invertible-hom-Precategory)
+
+  equiv-postcomp-hom-is-invertible-hom-Precategory :
+    hom-Precategory C z x ≃ hom-Precategory C z y
+  pr1 equiv-postcomp-hom-is-invertible-hom-Precategory =
+    postcomp-hom-Precategory C f z
+  pr2 equiv-postcomp-hom-is-invertible-hom-Precategory =
+    is-equiv-postcomp-hom-is-invertible-hom-Precategory
+
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  (f : invertible-hom-Precategory C x y)
+  (z : obj-Precategory C)
+  where
+
+  is-equiv-postcomp-hom-invertible-hom-Precategory :
+    is-equiv (postcomp-hom-Precategory C (hom-invertible-hom-Precategory C f) z)
+  is-equiv-postcomp-hom-invertible-hom-Precategory =
+    is-equiv-postcomp-hom-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory C f)
+      ( z)
+
+  equiv-postcomp-hom-invertible-hom-Precategory :
+    hom-Precategory C z x ≃ hom-Precategory C z y
+  equiv-postcomp-hom-invertible-hom-Precategory =
+    equiv-postcomp-hom-is-invertible-hom-Precategory C
+      ( is-invertible-hom-iso-Precategory C f)
+      ( z)
+```
+
+### When `hom x y` is a proposition, The type of invertible morphisms from `x` to `y` is a proposition
+
+The type of invertible morphisms between objects `x y : A` is a subtype of `hom x y`, so
+when this type is a proposition, then the type of invertible morphisms from `x` to `y`
+form a proposition.
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  where
+
+  is-prop-invertible-hom-is-prop-hom-Precategory :
+    is-prop (hom-Precategory C x y) → is-prop (invertible-hom-Precategory C x y)
+  is-prop-invertible-hom-is-prop-hom-Precategory =
+    is-prop-type-subtype (is-invertible-hom-prop-Precategory C)
+
+  invertible-hom-prop-is-prop-hom-Precategory :
+    is-prop (hom-Precategory C x y) → Prop l2
+  pr1 (invertible-hom-prop-is-prop-hom-Precategory is-prop-hom-C-x-y) =
+    invertible-hom-Precategory C x y
+  pr2 (invertible-hom-prop-is-prop-hom-Precategory is-prop-hom-C-x-y) =
+    is-prop-invertible-hom-is-prop-hom-Precategory is-prop-hom-C-x-y
+```
+
+### When `hom x y` and `hom y x` are propositions, it suffices to provide a morphism in each direction to construct an invertible morphism
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  where
+
+  is-invertible-hom-is-prop-hom-Precategory' :
+    is-prop (hom-Precategory C x x) →
+    is-prop (hom-Precategory C y y) →
+    (f : hom-Precategory C x y) →
+    hom-Precategory C y x →
+    is-invertible-hom-Precategory C f
+  is-invertible-hom-is-prop-hom-Precategory' H K f g =
+    (g , eq-is-prop K , eq-is-prop H)
+
+  invertible-hom-is-prop-hom-Precategory' :
+    is-prop (hom-Precategory C x x) →
+    is-prop (hom-Precategory C y y) →
+    hom-Precategory C x y →
+    hom-Precategory C y x →
+    invertible-hom-Precategory C x y
+  pr1 (invertible-hom-is-prop-hom-Precategory' _ _ f g) = f
+  pr2 (invertible-hom-is-prop-hom-Precategory' H K f g) =
+    is-invertible-hom-is-prop-hom-Precategory' H K f g
+
+  is-invertible-hom-is-prop-hom-Precategory :
+    ((x' y' : obj-Precategory C) → is-prop (hom-Precategory C x' y')) →
+    (f : hom-Precategory C x y) → hom-Precategory C y x →
+    is-invertible-hom-Precategory C f
+  is-invertible-hom-is-prop-hom-Precategory H =
+    is-invertible-hom-is-prop-hom-Precategory' (H x x) (H y y)
+
+  invertible-hom-is-prop-hom-Precategory :
+    ((x' y' : obj-Precategory C) → is-prop (hom-Precategory C x' y')) →
+    hom-Precategory C x y →
+    hom-Precategory C y x →
+    invertible-hom-Precategory C x y
+  invertible-hom-is-prop-hom-Precategory H =
+    invertible-hom-is-prop-hom-Precategory' (H x x) (H y y)
+```
+
+### Functoriality of `invertible-hom-eq`
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y z : obj-Precategory C}
+  where
+
+  preserves-concat-invertible-hom-eq-Precategory :
+    (p : x ＝ y) (q : y ＝ z) →
+    invertible-hom-eq-Precategory C x z (p ∙ q) ＝
+    comp-invertible-hom-Precategory C
+      ( invertible-hom-eq-Precategory C y z q)
+      ( invertible-hom-eq-Precategory C x y p)
+  preserves-concat-invertible-hom-eq-Precategory refl q =
+    inv
+      ( right-unit-law-comp-invertible-hom-Precategory C
+        ( invertible-hom-eq-Precategory C y z q))
+```
diff --git a/src/category-theory/isomorphisms-in-precategories.lagda.md b/src/category-theory/isomorphisms-in-precategories.lagda.md
index 4e7be2a906..819ca73128 100644
--- a/src/category-theory/isomorphisms-in-precategories.lagda.md
+++ b/src/category-theory/isomorphisms-in-precategories.lagda.md
@@ -8,6 +8,8 @@ module category-theory.isomorphisms-in-precategories where
 
 ```agda
 open import category-theory.precategories
+open import category-theory.retractions-in-precategories
+open import category-theory.sections-in-precategories
 
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
@@ -22,6 +24,7 @@ open import foundation.retractions
 open import foundation.sections
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 
@@ -29,49 +32,111 @@ open import foundation.universe-levels
 
 ## Idea
 
-An **isomorphism** in a [precategory](category-theory.precategories.md) `C` is a
-morphism `f : x → y` in `C` for which there exists a morphism `g : y → x` such
-that `f ∘ g ＝ id` and `g ∘ f ＝ id`.
+An {{#concept "isomorphism" Disambiguation="precategory" Agda=iso-Precategory}}
+in a [precategory](category-theory.precategories.md) `C` is a
+morphism `f : x → y` in `C` which has a [section](category-theory.sections-in-precategories.md) and a [retraction](category-theory.retractions-in-precategories.md). In other words, an isomorphism is a morphism `f : x → y` for which there is a morphism `g : y → x` equipped with an identification
+
+```text
+  f ∘ g ＝ id,
+```
+
+and a morphism `h : y → x` equipped with an identification
+
+```text
+  h ∘ f ＝ id.
+```
+
+This definition of isomorphisms follows a general pattern in agda-unimath, where we will always define isomorphisms in this manner.
 
 ## Definitions
 
 ### The predicate of being an isomorphism in a precategory
 
 ```agda
-is-iso-Precategory :
-  {l1 l2 : Level}
-  (C : Precategory l1 l2)
-  {x y : obj-Precategory C}
-  (f : hom-Precategory C x y) →
-  UU l2
-is-iso-Precategory C {x} {y} f =
-  Σ ( hom-Precategory C y x)
-    ( λ g →
-      ( comp-hom-Precategory C f g ＝ id-hom-Precategory C) ×
-      ( comp-hom-Precategory C g f ＝ id-hom-Precategory C))
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} (f : hom-Precategory C x y)
+  where
+  
+  is-iso-Precategory : UU l2
+  is-iso-Precategory =
+    section-hom-Precategory C f × retraction-hom-Precategory C f
 
 module _
-  {l1 l2 : Level}
-  (C : Precategory l1 l2)
-  {x y : obj-Precategory C}
-  {f : hom-Precategory C x y}
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} {f : hom-Precategory C x y}
+  (H : is-iso-Precategory C f)
   where
 
-  hom-inv-is-iso-Precategory :
-    is-iso-Precategory C f → hom-Precategory C y x
-  hom-inv-is-iso-Precategory = pr1
+  section-is-iso-Precategory : section-hom-Precategory C f
+  section-is-iso-Precategory = pr1 H
+
+  hom-section-is-iso-Precategory : hom-Precategory C y x
+  hom-section-is-iso-Precategory =
+    hom-section-hom-Precategory C f section-is-iso-Precategory
+
+  is-section-section-is-iso-Precategory :
+    is-section-hom-Precategory C f hom-section-is-iso-Precategory
+  is-section-section-is-iso-Precategory =
+    is-section-section-hom-Precategory C f section-is-iso-Precategory
+
+  retraction-is-iso-Precategory : retraction-hom-Precategory C f
+  retraction-is-iso-Precategory = pr2 H
+
+  hom-retraction-is-iso-Precategory : hom-Precategory C y x
+  hom-retraction-is-iso-Precategory =
+    hom-retraction-hom-Precategory C f retraction-is-iso-Precategory
+
+  is-retraction-retraction-is-iso-Precategory :
+    is-retraction-hom-Precategory C f hom-retraction-is-iso-Precategory
+  is-retraction-retraction-is-iso-Precategory =
+    is-retraction-retraction-hom-Precategory C f retraction-is-iso-Precategory
+
+  hom-inv-is-iso-Precategory : hom-Precategory C y x
+  hom-inv-is-iso-Precategory = hom-section-is-iso-Precategory
 
   is-section-hom-inv-is-iso-Precategory :
-    (H : is-iso-Precategory C f) →
-    comp-hom-Precategory C f (hom-inv-is-iso-Precategory H) ＝
-    id-hom-Precategory C
-  is-section-hom-inv-is-iso-Precategory = pr1 ∘ pr2
+    is-section-hom-Precategory C f hom-inv-is-iso-Precategory
+  is-section-hom-inv-is-iso-Precategory = is-section-section-is-iso-Precategory
+
+  eq-hom-retraction-hom-section-is-iso-Precategory :
+    hom-section-is-iso-Precategory ＝ hom-retraction-is-iso-Precategory
+  eq-hom-retraction-hom-section-is-iso-Precategory =
+    equational-reasoning
+      hom-section-is-iso-Precategory
+      ＝ comp-hom-Precategory C
+          ( id-hom-Precategory C)
+          ( hom-section-is-iso-Precategory)
+        by
+        inv (left-unit-law-comp-hom-Precategory C _)
+      ＝ comp-hom-Precategory C
+          ( comp-hom-Precategory C hom-retraction-is-iso-Precategory f)
+          ( hom-section-is-iso-Precategory)
+        by
+        inv
+          ( ap
+            ( λ g → comp-hom-Precategory C g _)
+            ( is-retraction-retraction-is-iso-Precategory))
+      ＝ comp-hom-Precategory C
+          ( hom-retraction-is-iso-Precategory)
+          ( comp-hom-Precategory C f hom-section-is-iso-Precategory)
+        by associative-comp-hom-Precategory C _ _ _
+      ＝ comp-hom-Precategory C
+          ( hom-retraction-is-iso-Precategory)
+          ( id-hom-Precategory C)
+        by
+        ap (comp-hom-Precategory C _) is-section-section-is-iso-Precategory
+      ＝ hom-retraction-is-iso-Precategory
+        by
+        right-unit-law-comp-hom-Precategory C _
 
   is-retraction-hom-inv-is-iso-Precategory :
-    (H : is-iso-Precategory C f) →
-    comp-hom-Precategory C (hom-inv-is-iso-Precategory H) f ＝
-    id-hom-Precategory C
-  is-retraction-hom-inv-is-iso-Precategory = pr2 ∘ pr2
+    is-retraction-hom-Precategory C f hom-inv-is-iso-Precategory
+  is-retraction-hom-inv-is-iso-Precategory =
+    tr
+      ( is-retraction-hom-Precategory C f)
+      ( inv eq-hom-retraction-hom-section-is-iso-Precategory)
+      ( is-retraction-retraction-is-iso-Precategory)
 ```
 
 ### Isomorphisms in a precategory
@@ -138,11 +203,13 @@ module _
   {x : obj-Precategory C}
   where
 
-  is-iso-id-hom-Precategory :
-    is-iso-Precategory C (id-hom-Precategory C {x})
-  pr1 is-iso-id-hom-Precategory = id-hom-Precategory C
+  is-iso-id-hom-Precategory : is-iso-Precategory C (id-hom-Precategory C {x})
+  pr1 (pr1 is-iso-id-hom-Precategory) =
+    id-hom-Precategory C
+  pr2 (pr1 is-iso-id-hom-Precategory) =
+    right-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
   pr1 (pr2 is-iso-id-hom-Precategory) =
-    left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
+    id-hom-Precategory C
   pr2 (pr2 is-iso-id-hom-Precategory) =
     left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
 
@@ -198,7 +265,7 @@ module _
     (f : hom-Precategory C x y)
     (H K : is-iso-Precategory C f) → H ＝ K
   all-elements-equal-is-iso-Precategory f
-    (g , p , q) (g' , p' , q') =
+    ((g , p) , (h , q)) ((g' , p') , (h' , q')) =
     eq-type-subtype
       ( λ g →
         product-Prop