From eda7bb2dc18c60aefab907696d3a7695f66cc0bf Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Tue, 19 Sep 2023 22:01:57 +0200
Subject: [PATCH] Isomorphisms in large categories and large precategories
 (#791)

---
 src/category-theory.lagda.md                  |   1 +
 ...imorphisms-in-large-precategories.lagda.md |  20 +-
 .../isomorphisms-in-large-categories.lagda.md | 623 ++++++++++++++++++
 ...omorphisms-in-large-precategories.lagda.md | 532 ++++++++++++---
 src/category-theory/large-categories.lagda.md |  20 +
 .../large-precategories.lagda.md              |  20 +
 ...omorphisms-in-large-precategories.lagda.md |  20 +-
 ...-isomorphisms-large-precategories.lagda.md |   6 -
 .../isomorphisms-group-actions.lagda.md       |  12 +-
 src/group-theory/isomorphisms-groups.lagda.md |   6 +-
 .../isomorphisms-semigroups.lagda.md          |  27 +-
 src/ring-theory/isomorphisms-rings.lagda.md   |  25 +-
 12 files changed, 1169 insertions(+), 143 deletions(-)
 create mode 100644 src/category-theory/isomorphisms-in-large-categories.lagda.md

diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index cdfdf3662d..f2e4e99f36 100644
--- a/src/category-theory.lagda.md
+++ b/src/category-theory.lagda.md
@@ -57,6 +57,7 @@ open import category-theory.groupoids public
 open import category-theory.homotopies-natural-transformations-large-precategories public
 open import category-theory.initial-objects-in-precategories public
 open import category-theory.isomorphisms-in-categories public
+open import category-theory.isomorphisms-in-large-categories public
 open import category-theory.isomorphisms-in-large-precategories public
 open import category-theory.isomorphisms-in-precategories public
 open import category-theory.large-categories public
diff --git a/src/category-theory/epimorphisms-in-large-precategories.lagda.md b/src/category-theory/epimorphisms-in-large-precategories.lagda.md
index 791366504f..6766641d4f 100644
--- a/src/category-theory/epimorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/epimorphisms-in-large-precategories.lagda.md
@@ -64,7 +64,7 @@ module _
   where
 
   is-epi-iso-Large-Precategory :
-    is-epi-Large-Precategory C l3 X Y (hom-iso-Large-Precategory C X Y f)
+    is-epi-Large-Precategory C l3 X Y (hom-iso-Large-Precategory C f)
   is-epi-iso-Large-Precategory Z g h =
     is-equiv-is-invertible
       ( λ P →
@@ -72,33 +72,33 @@ module _
           ( right-unit-law-comp-hom-Large-Precategory C g)) ∙
           ( ( ap
             ( λ h' → comp-hom-Large-Precategory C g h')
-            ( inv (is-section-hom-inv-iso-Large-Precategory C X Y f))) ∙
+            ( inv (is-section-hom-inv-iso-Large-Precategory C f))) ∙
             ( ( inv
               ( associative-comp-hom-Large-Precategory C
                 ( g)
-                ( hom-iso-Large-Precategory C X Y f)
-                ( hom-inv-iso-Large-Precategory C X Y f))) ∙
+                ( hom-iso-Large-Precategory C f)
+                ( hom-inv-iso-Large-Precategory C f))) ∙
               ( ( ap
                 ( λ h' →
                   comp-hom-Large-Precategory
                     ( C)
                     ( h')
-                    ( hom-inv-iso-Large-Precategory C X Y f))
+                    ( hom-inv-iso-Large-Precategory C f))
                 ( P)) ∙
                 ( ( associative-comp-hom-Large-Precategory C
                   ( h)
-                  ( hom-iso-Large-Precategory C X Y f)
-                  ( hom-inv-iso-Large-Precategory C X Y f)) ∙
+                  ( hom-iso-Large-Precategory C f)
+                  ( hom-inv-iso-Large-Precategory C f)) ∙
                   ( ( ap
                     ( comp-hom-Large-Precategory C h)
-                    ( is-section-hom-inv-iso-Large-Precategory C X Y f)) ∙
+                    ( is-section-hom-inv-iso-Large-Precategory C f)) ∙
                     ( right-unit-law-comp-hom-Large-Precategory C h)))))))
       ( λ p →
         eq-is-prop
           ( is-set-type-hom-Large-Precategory C X Z
             ( comp-hom-Large-Precategory C g
-              ( hom-iso-Large-Precategory C X Y f))
+              ( hom-iso-Large-Precategory C f))
             ( comp-hom-Large-Precategory C h
-              ( hom-iso-Large-Precategory C X Y f))))
+              ( hom-iso-Large-Precategory C f))))
       ( λ p → eq-is-prop (is-set-type-hom-Large-Precategory C Y Z g h))
 ```
diff --git a/src/category-theory/isomorphisms-in-large-categories.lagda.md b/src/category-theory/isomorphisms-in-large-categories.lagda.md
new file mode 100644
index 0000000000..06d6614938
--- /dev/null
+++ b/src/category-theory/isomorphisms-in-large-categories.lagda.md
@@ -0,0 +1,623 @@
+# Isomorphisms in large categories
+
+```agda
+module category-theory.isomorphisms-in-large-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.isomorphisms-in-categories
+open import category-theory.isomorphisms-in-large-precategories
+open import category-theory.large-categories
+
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An **isomorphism** in a [large category](category-theory.large-categories.md)
+`C` is a morphism `f : X → Y` in `C` for which there is an inverse, i.e., for
+which there exists a morphism `g : Y → X` such that `f ∘ g ＝ id` and
+`g ∘ f ＝ id`.
+
+## Definitions
+
+### The predicate of being an isomorphism
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  (f : type-hom-Large-Category C X Y)
+  where
+
+  is-iso-hom-Large-Category : UU (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
+  is-iso-hom-Large-Category =
+    is-iso-hom-Large-Precategory (large-precategory-Large-Category C) f
+
+  hom-inv-is-iso-hom-Large-Category :
+    is-iso-hom-Large-Category → type-hom-Large-Category C Y X
+  hom-inv-is-iso-hom-Large-Category =
+    hom-inv-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+
+  is-section-hom-inv-is-iso-hom-Large-Category :
+    (H : is-iso-hom-Large-Category) →
+    comp-hom-Large-Category C f (hom-inv-is-iso-hom-Large-Category H) ＝
+    id-hom-Large-Category C
+  is-section-hom-inv-is-iso-hom-Large-Category =
+    is-section-hom-inv-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+
+  is-retraction-hom-inv-is-iso-hom-Large-Category :
+    (H : is-iso-hom-Large-Category) →
+    comp-hom-Large-Category C (hom-inv-is-iso-hom-Large-Category H) f ＝
+    id-hom-Large-Category C
+  is-retraction-hom-inv-is-iso-hom-Large-Category =
+    is-retraction-hom-inv-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+```
+
+### Isomorphisms in a large category
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  (X : obj-Large-Category C l1) (Y : obj-Large-Category C l2)
+  where
+
+  iso-Large-Category : UU (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2)
+  iso-Large-Category =
+    iso-Large-Precategory (large-precategory-Large-Category C) X Y
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  (f : iso-Large-Category C X Y)
+  where
+
+  hom-iso-Large-Category : type-hom-Large-Category C X Y
+  hom-iso-Large-Category =
+    hom-iso-Large-Precategory (large-precategory-Large-Category C) f
+
+  is-iso-iso-Large-Category :
+    is-iso-hom-Large-Category C hom-iso-Large-Category
+  is-iso-iso-Large-Category =
+    is-iso-iso-Large-Precategory (large-precategory-Large-Category C) f
+
+  hom-inv-iso-Large-Category : type-hom-Large-Category C Y X
+  hom-inv-iso-Large-Category =
+    hom-inv-iso-Large-Precategory (large-precategory-Large-Category C) f
+
+  is-section-hom-inv-iso-Large-Category :
+    ( comp-hom-Large-Category C
+      ( hom-iso-Large-Category)
+      ( hom-inv-iso-Large-Category)) ＝
+    ( id-hom-Large-Category C)
+  is-section-hom-inv-iso-Large-Category =
+    is-section-hom-inv-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+
+  is-retraction-hom-inv-iso-Large-Category :
+    ( comp-hom-Large-Category C
+      ( hom-inv-iso-Large-Category)
+      ( hom-iso-Large-Category)) ＝
+    ( id-hom-Large-Category C)
+  is-retraction-hom-inv-iso-Large-Category =
+    is-retraction-hom-inv-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+```
+
+## Examples
+
+### The identity morphisms are isomorphisms
+
+For any object `x : A`, the identity morphism `id_x : hom x x` is an isomorphism
+from `x` to `x` since `id_x ∘ id_x = id_x` (it is its own inverse).
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 : Level} {X : obj-Large-Category C l1}
+  where
+
+  is-iso-id-hom-Large-Category :
+    is-iso-hom-Large-Category C (id-hom-Large-Category C {X = X})
+  is-iso-id-hom-Large-Category =
+    is-iso-id-hom-Large-Precategory (large-precategory-Large-Category C)
+
+  id-iso-Large-Category : iso-Large-Category C X X
+  id-iso-Large-Category =
+    id-iso-Large-Precategory (large-precategory-Large-Category C)
+```
+
+### Equalities give rise to isomorphisms
+
+An equality between objects `X Y : A` gives rise to an isomorphism between them.
+This is because by the J-rule, it is enough to construct an isomorphism given
+`refl : X ＝ X`, from `X` to itself. We take the identity morphism as such an
+isomorphism.
+
+```agda
+iso-eq-Large-Category :
+  {α : Level → Level} {β : Level → Level → Level} →
+  (C : Large-Category α β) {l1 : Level}
+  (X : obj-Large-Category C l1) (Y : obj-Large-Category C l1) →
+  X ＝ Y → iso-Large-Category C X Y
+iso-eq-Large-Category C =
+  iso-eq-Large-Precategory (large-precategory-Large-Category C)
+
+compute-iso-eq-Large-Category :
+  {α : Level → Level} {β : Level → Level → Level} →
+  (C : Large-Category α β) {l1 : Level}
+  (X : obj-Large-Category C l1) (Y : obj-Large-Category C l1) →
+  iso-eq-Category (category-Large-Category C l1) {X} {Y} ~
+  iso-eq-Large-Category C X Y
+compute-iso-eq-Large-Category C X .X refl = refl
+```
+
+## Properties
+
+### Being an isomorphism is a proposition
+
+Let `f : hom x y` and suppose `g g' : hom y x` are both two-sided inverses to
+`f`. It is enough to show that `g = g'` since the equalities are propositions
+(since the hom-types are sets). But we have the following chain of equalities:
+`g = g ∘ id_y = g ∘ (f ∘ g') = (g ∘ f) ∘ g' = id_x ∘ g' = g'`.
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  where
+
+  all-elements-equal-is-iso-hom-Large-Category :
+    (f : type-hom-Large-Category C X Y)
+    (H K : is-iso-hom-Large-Category C f) → H ＝ K
+  all-elements-equal-is-iso-hom-Large-Category =
+    all-elements-equal-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+
+  is-prop-is-iso-hom-Large-Category :
+    (f : type-hom-Large-Category C X Y) →
+    is-prop (is-iso-hom-Large-Category C f)
+  is-prop-is-iso-hom-Large-Category f =
+    is-prop-all-elements-equal
+      ( all-elements-equal-is-iso-hom-Large-Category f)
+
+  is-iso-prop-hom-Large-Category :
+    (f : type-hom-Large-Category C X Y) → Prop (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
+  is-iso-prop-hom-Large-Category =
+    is-iso-prop-hom-Large-Precategory (large-precategory-Large-Category C)
+```
+
+### Equality of isomorphism is equality of their underlying morphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  where
+
+  eq-iso-eq-hom-Large-Category :
+    (f g : iso-Large-Category C X Y) →
+    hom-iso-Large-Category C f ＝ hom-iso-Large-Category C g → f ＝ g
+  eq-iso-eq-hom-Large-Category =
+    eq-iso-eq-hom-Large-Precategory (large-precategory-Large-Category C)
+```
+
+### The type of isomorphisms form a set
+
+The type of isomorphisms between objects `x y : A` is a subtype of the set
+`hom x y` since being an isomorphism is a proposition.
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  where
+
+  is-set-iso-Large-Category : is-set (iso-Large-Category C X Y)
+  is-set-iso-Large-Category =
+    is-set-iso-Large-Precategory (large-precategory-Large-Category C)
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  (X : obj-Large-Category C l1) (Y : obj-Large-Category C l2)
+  where
+
+  iso-set-Large-Category : Set (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2)
+  iso-set-Large-Category =
+    iso-set-Large-Precategory (large-precategory-Large-Category C) X Y
+```
+
+### Isomorphisms are closed under composition
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 l3 : Level}
+  {X : obj-Large-Category C l1}
+  {Y : obj-Large-Category C l2}
+  {Z : obj-Large-Category C l3}
+  {g : type-hom-Large-Category C Y Z}
+  {f : type-hom-Large-Category C X Y}
+  where
+
+  hom-comp-is-iso-hom-Large-Category :
+    is-iso-hom-Large-Category C g →
+    is-iso-hom-Large-Category C f →
+    type-hom-Large-Category C Z X
+  hom-comp-is-iso-hom-Large-Category =
+    hom-comp-is-iso-hom-Large-Precategory (large-precategory-Large-Category C)
+
+  is-section-comp-is-iso-hom-Large-Category :
+    (q : is-iso-hom-Large-Category C g)
+    (p : is-iso-hom-Large-Category C f) →
+    comp-hom-Large-Category C
+      ( comp-hom-Large-Category C g f)
+      ( hom-comp-is-iso-hom-Large-Category q p) ＝
+    id-hom-Large-Category C
+  is-section-comp-is-iso-hom-Large-Category =
+    is-section-comp-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+
+  is-retraction-comp-is-iso-hom-Large-Category :
+    (q : is-iso-hom-Large-Category C g)
+    (p : is-iso-hom-Large-Category C f) →
+    comp-hom-Large-Category C
+      ( hom-comp-is-iso-hom-Large-Category q p)
+      ( comp-hom-Large-Category C g f) ＝
+    id-hom-Large-Category C
+  is-retraction-comp-is-iso-hom-Large-Category =
+    is-retraction-comp-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+
+  is-iso-comp-is-iso-hom-Large-Category :
+    is-iso-hom-Large-Category C g → is-iso-hom-Large-Category C f →
+    is-iso-hom-Large-Category C (comp-hom-Large-Category C g f)
+  is-iso-comp-is-iso-hom-Large-Category =
+    is-iso-comp-is-iso-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+```
+
+### Composition of isomorphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 l3 : Level}
+  {X : obj-Large-Category C l1}
+  {Y : obj-Large-Category C l2}
+  {Z : obj-Large-Category C l3}
+  (g : iso-Large-Category C Y Z)
+  (f : iso-Large-Category C X Y)
+  where
+
+  hom-comp-iso-Large-Category :
+    type-hom-Large-Category C X Z
+  hom-comp-iso-Large-Category =
+    hom-comp-iso-Large-Precategory (large-precategory-Large-Category C) g f
+
+  is-iso-comp-iso-Large-Category :
+    is-iso-hom-Large-Category C hom-comp-iso-Large-Category
+  is-iso-comp-iso-Large-Category =
+    is-iso-comp-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( g)
+      ( f)
+
+  comp-iso-Large-Category :
+    iso-Large-Category C X Z
+  comp-iso-Large-Category =
+    comp-iso-Large-Precategory (large-precategory-Large-Category C) g f
+
+  hom-inv-comp-iso-Large-Category :
+    type-hom-Large-Category C Z X
+  hom-inv-comp-iso-Large-Category =
+    hom-inv-iso-Large-Category C comp-iso-Large-Category
+
+  is-section-inv-comp-iso-Large-Category :
+    comp-hom-Large-Category C
+      ( hom-comp-iso-Large-Category)
+      ( hom-inv-comp-iso-Large-Category) ＝
+    id-hom-Large-Category C
+  is-section-inv-comp-iso-Large-Category =
+    is-section-hom-inv-iso-Large-Category C comp-iso-Large-Category
+
+  is-retraction-inv-comp-iso-Large-Category :
+    comp-hom-Large-Category C
+      ( hom-inv-comp-iso-Large-Category)
+      ( hom-comp-iso-Large-Category) ＝
+    id-hom-Large-Category C
+  is-retraction-inv-comp-iso-Large-Category =
+    is-retraction-hom-inv-iso-Large-Category C comp-iso-Large-Category
+```
+
+### Inverses of isomorphisms are isomorphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  {f : type-hom-Large-Category C X Y}
+  where
+
+  is-iso-inv-is-iso-hom-Large-Category :
+    (p : is-iso-hom-Large-Category C f) →
+    is-iso-hom-Large-Category C (hom-inv-iso-Large-Category C (f , p))
+  pr1 (is-iso-inv-is-iso-hom-Large-Category p) = f
+  pr1 (pr2 (is-iso-inv-is-iso-hom-Large-Category p)) =
+    is-retraction-hom-inv-is-iso-hom-Large-Category C f p
+  pr2 (pr2 (is-iso-inv-is-iso-hom-Large-Category p)) =
+    is-section-hom-inv-is-iso-hom-Large-Category C f p
+```
+
+### Inverses of isomorphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  where
+
+  inv-iso-Large-Category :
+    iso-Large-Category C X Y →
+    iso-Large-Category C Y X
+  pr1 (inv-iso-Large-Category f) = hom-inv-iso-Large-Category C f
+  pr2 (inv-iso-Large-Category f) =
+    is-iso-inv-is-iso-hom-Large-Category C
+      ( is-iso-iso-Large-Category C f)
+```
+
+### Composition of isomorphisms satisfies the unit laws
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  (f : iso-Large-Category C X Y)
+  where
+
+  left-unit-law-comp-iso-Large-Category :
+    comp-iso-Large-Category C (id-iso-Large-Category C) f ＝ f
+  left-unit-law-comp-iso-Large-Category =
+    left-unit-law-comp-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+
+  right-unit-law-comp-iso-Large-Category :
+    comp-iso-Large-Category C f (id-iso-Large-Category C) ＝ f
+  right-unit-law-comp-iso-Large-Category =
+    right-unit-law-comp-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+```
+
+### Composition of isomorphisms is associative
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 l3 l4 : Level}
+  {X : obj-Large-Category C l1}
+  {Y : obj-Large-Category C l2}
+  {Z : obj-Large-Category C l3}
+  {W : obj-Large-Category C l4}
+  (h : iso-Large-Category C Z W)
+  (g : iso-Large-Category C Y Z)
+  (f : iso-Large-Category C X Y)
+  where
+
+  associative-comp-iso-Large-Category :
+    comp-iso-Large-Category C (comp-iso-Large-Category C h g) f ＝
+    comp-iso-Large-Category C h (comp-iso-Large-Category C g f)
+  associative-comp-iso-Large-Category =
+    associative-comp-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( h)
+      ( g)
+      ( f)
+```
+
+### Composition of isomorphisms satisfies inverse laws
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  (f : iso-Large-Category C X Y)
+  where
+
+  left-inverse-law-comp-iso-Large-Category :
+    comp-iso-Large-Category C (inv-iso-Large-Category C f) f ＝
+    id-iso-Large-Category C
+  left-inverse-law-comp-iso-Large-Category =
+    left-inverse-law-comp-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+
+  right-inverse-law-comp-iso-Large-Category :
+    comp-iso-Large-Category C f (inv-iso-Large-Category C f) ＝
+    id-iso-Large-Category C
+  right-inverse-law-comp-iso-Large-Category =
+    right-inverse-law-comp-iso-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( f)
+```
+
+### A morphism `f` is an isomorphism if and only if precomposition by `f` is an equivalence
+
+**Proof:** If `f` is an isomorphism 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 _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  {f : type-hom-Large-Category C X Y}
+  (H :
+    {l3 : Level} (Z : obj-Large-Category C l3) →
+    is-equiv (precomp-hom-Large-Category C f Z))
+  where
+
+  hom-inv-is-iso-is-equiv-precomp-hom-Large-Category :
+    type-hom-Large-Category C Y X
+  hom-inv-is-iso-is-equiv-precomp-hom-Large-Category =
+    hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+
+  is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Category :
+    comp-hom-Large-Category C
+      ( hom-inv-is-iso-is-equiv-precomp-hom-Large-Category)
+      ( f) ＝
+    id-hom-Large-Category C
+  is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Category =
+    is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+
+  is-section-hom-inv-is-iso-is-equiv-precomp-hom-Large-Category :
+    comp-hom-Large-Category C
+      ( f)
+      ( hom-inv-is-iso-is-equiv-precomp-hom-Large-Category) ＝
+    id-hom-Large-Category C
+  is-section-hom-inv-is-iso-is-equiv-precomp-hom-Large-Category =
+    is-section-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+
+  is-iso-is-equiv-precomp-hom-Large-Category :
+    is-iso-hom-Large-Category C f
+  is-iso-is-equiv-precomp-hom-Large-Category =
+    is-iso-is-equiv-precomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+```
+
+### A morphism `f` is an isomorphism if and only if postcomposition by `f` is an equivalence
+
+**Proof:** If `f` is an isomorphism 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 _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Category α β) {l1 l2 : Level}
+  {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
+  {f : type-hom-Large-Category C X Y}
+  (H :
+    {l3 : Level} (Z : obj-Large-Category C l3) →
+    is-equiv (postcomp-hom-Large-Category C Z f))
+  where
+
+  hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category :
+    type-hom-Large-Category C Y X
+  hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category =
+    hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+
+  is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category :
+    comp-hom-Large-Category C
+      ( f)
+      ( hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category) ＝
+    id-hom-Large-Category C
+  is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category =
+    is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+
+  is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category :
+    comp-hom-Large-Category C
+      ( hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category)
+      ( f) ＝
+    id-hom-Large-Category C
+  is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category =
+    is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+
+  is-iso-is-equiv-postcomp-hom-Large-Category :
+    is-iso-hom-Large-Category C f
+  is-iso-is-equiv-postcomp-hom-Large-Category =
+    is-iso-is-equiv-postcomp-hom-Large-Precategory
+      ( large-precategory-Large-Category C)
+      ( H)
+```
diff --git a/src/category-theory/isomorphisms-in-large-precategories.lagda.md b/src/category-theory/isomorphisms-in-large-precategories.lagda.md
index 508526479a..64dc104922 100644
--- a/src/category-theory/isomorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/isomorphisms-in-large-precategories.lagda.md
@@ -13,9 +13,11 @@ open import category-theory.large-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.sets
 open import foundation.subtypes
@@ -26,13 +28,12 @@ open import foundation.universe-levels
 
 ## Idea
 
-An isomorphism between objects `x y : A` in a precategory `C` is a morphism
-`f : hom x y` for which there exists a morphism `g : hom y x` such that
+An **isomorphism** in a
+[large precategory](category-theory.large-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`.
 
-- `G ∘ F = id_x` and
-- `F ∘ G = id_y`.
-
-## Definition
+## Definitions
 
 ### The predicate of being an isomorphism
 
@@ -81,34 +82,36 @@ module _
   iso-Large-Precategory =
     Σ (type-hom-Large-Precategory C X Y) (is-iso-hom-Large-Precategory C)
 
-  hom-iso-Large-Precategory :
-    iso-Large-Precategory → type-hom-Large-Precategory C X Y
-  hom-iso-Large-Precategory = pr1
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  (f : iso-Large-Precategory C X Y)
+  where
+
+  hom-iso-Large-Precategory : type-hom-Large-Precategory C X Y
+  hom-iso-Large-Precategory = pr1 f
 
   is-iso-iso-Large-Precategory :
-    (f : iso-Large-Precategory) →
-    is-iso-hom-Large-Precategory C (hom-iso-Large-Precategory f)
-  is-iso-iso-Large-Precategory f = pr2 f
+    is-iso-hom-Large-Precategory C hom-iso-Large-Precategory
+  is-iso-iso-Large-Precategory = pr2 f
 
-  hom-inv-iso-Large-Precategory :
-    iso-Large-Precategory → type-hom-Large-Precategory C Y X
-  hom-inv-iso-Large-Precategory f = pr1 (pr2 f)
+  hom-inv-iso-Large-Precategory : type-hom-Large-Precategory C Y X
+  hom-inv-iso-Large-Precategory = pr1 (pr2 f)
 
   is-section-hom-inv-iso-Large-Precategory :
-    (f : iso-Large-Precategory) →
     ( comp-hom-Large-Precategory C
-      ( hom-iso-Large-Precategory f)
-      ( hom-inv-iso-Large-Precategory f)) ＝
+      ( hom-iso-Large-Precategory)
+      ( hom-inv-iso-Large-Precategory)) ＝
     ( id-hom-Large-Precategory C)
-  is-section-hom-inv-iso-Large-Precategory f = pr1 (pr2 (pr2 f))
+  is-section-hom-inv-iso-Large-Precategory = pr1 (pr2 (pr2 f))
 
   is-retraction-hom-inv-iso-Large-Precategory :
-    (f : iso-Large-Precategory) →
     ( comp-hom-Large-Precategory C
-      ( hom-inv-iso-Large-Precategory f)
-      ( hom-iso-Large-Precategory f)) ＝
+      ( hom-inv-iso-Large-Precategory)
+      ( hom-iso-Large-Precategory)) ＝
     ( id-hom-Large-Precategory C)
-  is-retraction-hom-inv-iso-Large-Precategory f = pr2 (pr2 (pr2 f))
+  is-retraction-hom-inv-iso-Large-Precategory = pr2 (pr2 (pr2 f))
 ```
 
 ## Examples
@@ -139,9 +142,9 @@ module _
 
 ### Equalities give rise to isomorphisms
 
-An equality between objects `x y : A` gives rise to an isomorphism between them.
+An equality between objects `X Y : A` gives rise to an isomorphism between them.
 This is because by the J-rule, it is enough to construct an isomorphism given
-`refl : Id x x`, from `x` to itself. We take the identity morphism as such an
+`refl : X ＝ X`, from `X` to itself. We take the identity morphism as such an
 isomorphism.
 
 ```agda
@@ -174,7 +177,7 @@ Let `f : hom x y` and suppose `g g' : hom y x` are both two-sided inverses to
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level}
-  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
   where
 
   all-elements-equal-is-iso-hom-Large-Precategory :
@@ -214,6 +217,22 @@ module _
     is-prop-is-iso-hom-Large-Precategory f
 ```
 
+### Equality of isomorphism is equality of their underlying morphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  where
+
+  eq-iso-eq-hom-Large-Precategory :
+    (f g : iso-Large-Precategory C X Y) →
+    hom-iso-Large-Precategory C f ＝ hom-iso-Large-Precategory C g → f ＝ g
+  eq-iso-eq-hom-Large-Precategory f g =
+    eq-type-subtype (is-iso-prop-hom-Large-Precategory C)
+```
+
 ### The type of isomorphisms form a set
 
 The type of isomorphisms between objects `x y : A` is a subtype of the set
@@ -223,117 +242,438 @@ The type of isomorphisms between objects `x y : A` is a subtype of the set
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level}
-  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
   where
 
   is-set-iso-Large-Precategory : is-set (iso-Large-Precategory C X Y)
   is-set-iso-Large-Precategory =
     is-set-type-subtype
-      ( is-iso-prop-hom-Large-Precategory C X Y)
+      ( is-iso-prop-hom-Large-Precategory C)
       ( is-set-type-hom-Large-Precategory C X Y)
 
-  iso-Large-Precategory-Set : Set (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2)
-  pr1 iso-Large-Precategory-Set = iso-Large-Precategory C X Y
-  pr2 iso-Large-Precategory-Set = is-set-iso-Large-Precategory
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
+  where
+
+  iso-set-Large-Precategory : Set (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2)
+  pr1 iso-set-Large-Precategory = iso-Large-Precategory C X Y
+  pr2 iso-set-Large-Precategory = is-set-iso-Large-Precategory C
 ```
 
-### Isomorphisms are stable by composition
+### Isomorphisms are closed under composition
 
 ```agda
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 l3 : Level}
-  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
-  (Z : obj-Large-Precategory C l3)
+  {X : obj-Large-Precategory C l1}
+  {Y : obj-Large-Precategory C l2}
+  {Z : obj-Large-Precategory C l3}
+  {g : type-hom-Large-Precategory C Y Z}
+  {f : type-hom-Large-Precategory C X Y}
   where
 
-  is-iso-comp-iso-Large-Precategory :
-    (g : type-hom-Large-Precategory C Y Z) →
-    (f : type-hom-Large-Precategory C X Y) →
-    is-iso-hom-Large-Precategory C g → is-iso-hom-Large-Precategory C f →
-    is-iso-hom-Large-Precategory C (comp-hom-Large-Precategory C g f)
-  pr1 (is-iso-comp-iso-Large-Precategory g f q p) =
+  hom-comp-is-iso-hom-Large-Precategory :
+    is-iso-hom-Large-Precategory C g →
+    is-iso-hom-Large-Precategory C f →
+    type-hom-Large-Precategory C Z X
+  hom-comp-is-iso-hom-Large-Precategory q p =
+    comp-hom-Large-Precategory C
+      ( hom-inv-is-iso-hom-Large-Precategory C f p)
+      ( hom-inv-is-iso-hom-Large-Precategory C g q)
+
+  is-section-comp-is-iso-hom-Large-Precategory :
+    (q : is-iso-hom-Large-Precategory C g)
+    (p : is-iso-hom-Large-Precategory C f) →
     comp-hom-Large-Precategory C
-      ( hom-inv-iso-Large-Precategory C X Y (pair f p))
-      ( hom-inv-iso-Large-Precategory C Y Z (pair g q))
-  pr1 (pr2 (is-iso-comp-iso-Large-Precategory g f q p)) =
-    ( associative-comp-hom-Large-Precategory C g f
-      ( pr1 (is-iso-comp-iso-Large-Precategory g f q p))) ∙
-      ( ( ap
-        ( comp-hom-Large-Precategory C g)
-        ( ( inv
+      ( comp-hom-Large-Precategory C g f)
+      ( hom-comp-is-iso-hom-Large-Precategory q p) ＝
+    id-hom-Large-Precategory C
+  is-section-comp-is-iso-hom-Large-Precategory q p =
+    ( associative-comp-hom-Large-Precategory C g f _) ∙
+    ( ap
+      ( comp-hom-Large-Precategory C g)
+      ( ( inv
           ( associative-comp-hom-Large-Precategory C f
-            ( hom-inv-iso-Large-Precategory C X Y (pair f p))
-            ( hom-inv-iso-Large-Precategory C Y Z (pair g q)))) ∙
-          ( ( ap
-            ( λ h →
-              comp-hom-Large-Precategory C h
-                (hom-inv-iso-Large-Precategory C Y Z (pair g q)))
-            ( is-section-hom-inv-iso-Large-Precategory C X Y (pair f p))) ∙
-            ( left-unit-law-comp-hom-Large-Precategory C
-              ( hom-inv-iso-Large-Precategory C Y Z (pair g q)))))) ∙
-        ( is-section-hom-inv-iso-Large-Precategory C Y Z (pair g q)))
-  pr2 (pr2 (is-iso-comp-iso-Large-Precategory g f q p)) =
+            ( hom-inv-is-iso-hom-Large-Precategory C f p)
+            ( hom-inv-is-iso-hom-Large-Precategory C g q))) ∙
+        ( ap
+          ( λ h → comp-hom-Large-Precategory C h _)
+          ( is-section-hom-inv-is-iso-hom-Large-Precategory C f p) ∙
+        ( left-unit-law-comp-hom-Large-Precategory C
+          ( hom-inv-is-iso-hom-Large-Precategory C g q))))) ∙
+    ( is-section-hom-inv-is-iso-hom-Large-Precategory C g q)
+
+  is-retraction-comp-is-iso-hom-Large-Precategory :
+    (q : is-iso-hom-Large-Precategory C g)
+    (p : is-iso-hom-Large-Precategory C f) →
+    comp-hom-Large-Precategory C
+      ( hom-comp-is-iso-hom-Large-Precategory q p)
+      ( comp-hom-Large-Precategory C g f) ＝
+    id-hom-Large-Precategory C
+  is-retraction-comp-is-iso-hom-Large-Precategory q p =
     ( associative-comp-hom-Large-Precategory C
-      ( hom-inv-iso-Large-Precategory C X Y (pair f p))
-      ( hom-inv-iso-Large-Precategory C Y Z (pair g q))
+      ( hom-inv-is-iso-hom-Large-Precategory C f p)
+      ( hom-inv-is-iso-hom-Large-Precategory C g q)
       ( comp-hom-Large-Precategory C g f)) ∙
-      ( ( ap
-        ( comp-hom-Large-Precategory
-          ( C)
-          ( hom-inv-iso-Large-Precategory C X Y (pair f p)))
-        ( ( inv
+    ( ap
+      ( comp-hom-Large-Precategory
+        ( C)
+        ( hom-inv-is-iso-hom-Large-Precategory C f p))
+      ( ( inv
           ( associative-comp-hom-Large-Precategory C
-            ( hom-inv-iso-Large-Precategory C Y Z (pair g q))
+            ( hom-inv-is-iso-hom-Large-Precategory C g q)
             ( g)
             ( f))) ∙
-          ( ( ap
+        ( ap
             ( λ h → comp-hom-Large-Precategory C h f)
-            ( is-retraction-hom-inv-iso-Large-Precategory C Y Z (pair g q))) ∙
-            ( left-unit-law-comp-hom-Large-Precategory C f)))) ∙
-        ( is-retraction-hom-inv-iso-Large-Precategory C X Y (pair f p)))
+            ( is-retraction-hom-inv-is-iso-hom-Large-Precategory C g q)) ∙
+        ( left-unit-law-comp-hom-Large-Precategory C f))) ∙
+    ( is-retraction-hom-inv-is-iso-hom-Large-Precategory C f p)
+
+  is-iso-comp-is-iso-hom-Large-Precategory :
+    is-iso-hom-Large-Precategory C g → is-iso-hom-Large-Precategory C f →
+    is-iso-hom-Large-Precategory C (comp-hom-Large-Precategory C g f)
+  pr1 (is-iso-comp-is-iso-hom-Large-Precategory q p) =
+    hom-comp-is-iso-hom-Large-Precategory q p
+  pr1 (pr2 (is-iso-comp-is-iso-hom-Large-Precategory q p)) =
+    is-section-comp-is-iso-hom-Large-Precategory q p
+  pr2 (pr2 (is-iso-comp-is-iso-hom-Large-Precategory q p)) =
+    is-retraction-comp-is-iso-hom-Large-Precategory q p
+```
+
+### Composition of isomorphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 l3 : Level}
+  {X : obj-Large-Precategory C l1}
+  {Y : obj-Large-Precategory C l2}
+  {Z : obj-Large-Precategory C l3}
+  (g : iso-Large-Precategory C Y Z)
+  (f : iso-Large-Precategory C X Y)
+  where
+
+  hom-comp-iso-Large-Precategory :
+    type-hom-Large-Precategory C X Z
+  hom-comp-iso-Large-Precategory =
+    comp-hom-Large-Precategory C
+      ( hom-iso-Large-Precategory C g)
+      ( hom-iso-Large-Precategory C f)
+
+  is-iso-comp-iso-Large-Precategory :
+    is-iso-hom-Large-Precategory C hom-comp-iso-Large-Precategory
+  is-iso-comp-iso-Large-Precategory =
+    is-iso-comp-is-iso-hom-Large-Precategory C
+      ( is-iso-iso-Large-Precategory C g)
+      ( is-iso-iso-Large-Precategory C f)
 
   comp-iso-Large-Precategory :
-    iso-Large-Precategory C Y Z →
-    iso-Large-Precategory C X Y →
     iso-Large-Precategory C X Z
-  pr1 (comp-iso-Large-Precategory g f) =
+  pr1 comp-iso-Large-Precategory = hom-comp-iso-Large-Precategory
+  pr2 comp-iso-Large-Precategory = is-iso-comp-iso-Large-Precategory
+
+  hom-inv-comp-iso-Large-Precategory :
+    type-hom-Large-Precategory C Z X
+  hom-inv-comp-iso-Large-Precategory =
+    hom-inv-iso-Large-Precategory C comp-iso-Large-Precategory
+
+  is-section-inv-comp-iso-Large-Precategory :
+    comp-hom-Large-Precategory C
+      ( hom-comp-iso-Large-Precategory)
+      ( hom-inv-comp-iso-Large-Precategory) ＝
+    id-hom-Large-Precategory C
+  is-section-inv-comp-iso-Large-Precategory =
+    is-section-hom-inv-iso-Large-Precategory C comp-iso-Large-Precategory
+
+  is-retraction-inv-comp-iso-Large-Precategory :
     comp-hom-Large-Precategory C
-      ( hom-iso-Large-Precategory C Y Z g)
-      ( hom-iso-Large-Precategory C X Y f)
-  pr2 (comp-iso-Large-Precategory f g) =
-    is-iso-comp-iso-Large-Precategory
-      ( hom-iso-Large-Precategory C Y Z f)
-      ( hom-iso-Large-Precategory C X Y g)
-      ( is-iso-iso-Large-Precategory C Y Z f)
-      ( is-iso-iso-Large-Precategory C X Y g)
+      ( hom-inv-comp-iso-Large-Precategory)
+      ( hom-comp-iso-Large-Precategory) ＝
+    id-hom-Large-Precategory C
+  is-retraction-inv-comp-iso-Large-Precategory =
+    is-retraction-hom-inv-iso-Large-Precategory C comp-iso-Large-Precategory
 ```
 
-### Isomorphisms are stable by inversion
+### Inverses of isomorphisms are isomorphisms
 
 ```agda
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level}
-  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  {f : type-hom-Large-Precategory C X Y}
   where
 
-  is-iso-inv-iso-Large-Precategory :
-    (f : type-hom-Large-Precategory C X Y) →
+  is-iso-inv-is-iso-hom-Large-Precategory :
     (p : is-iso-hom-Large-Precategory C f) →
-    is-iso-hom-Large-Precategory C (hom-inv-iso-Large-Precategory C X Y (f , p))
-  pr1 (is-iso-inv-iso-Large-Precategory f p) = f
-  pr1 (pr2 (is-iso-inv-iso-Large-Precategory f p)) =
-    is-retraction-hom-inv-iso-Large-Precategory C X Y (pair f p)
-  pr2 (pr2 (is-iso-inv-iso-Large-Precategory f p)) =
-    is-section-hom-inv-iso-Large-Precategory C X Y (pair f p)
+    is-iso-hom-Large-Precategory C (hom-inv-iso-Large-Precategory C (f , p))
+  pr1 (is-iso-inv-is-iso-hom-Large-Precategory p) = f
+  pr1 (pr2 (is-iso-inv-is-iso-hom-Large-Precategory p)) =
+    is-retraction-hom-inv-is-iso-hom-Large-Precategory C f p
+  pr2 (pr2 (is-iso-inv-is-iso-hom-Large-Precategory p)) =
+    is-section-hom-inv-is-iso-hom-Large-Precategory C f p
+```
+
+### Inverses of isomorphisms
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  where
 
   inv-iso-Large-Precategory :
     iso-Large-Precategory C X Y →
     iso-Large-Precategory C Y X
-  pr1 (inv-iso-Large-Precategory f) = hom-inv-iso-Large-Precategory C X Y f
+  pr1 (inv-iso-Large-Precategory f) = hom-inv-iso-Large-Precategory C f
   pr2 (inv-iso-Large-Precategory f) =
-    is-iso-inv-iso-Large-Precategory
-      ( hom-iso-Large-Precategory C X Y f)
-      ( is-iso-iso-Large-Precategory C X Y f)
+    is-iso-inv-is-iso-hom-Large-Precategory C
+      ( is-iso-iso-Large-Precategory C f)
+```
+
+### Composition of isomorphisms satisfies the unit laws
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  (f : iso-Large-Precategory C X Y)
+  where
+
+  left-unit-law-comp-iso-Large-Precategory :
+    comp-iso-Large-Precategory C (id-iso-Large-Precategory C) f ＝ f
+  left-unit-law-comp-iso-Large-Precategory =
+    eq-iso-eq-hom-Large-Precategory C
+      ( comp-iso-Large-Precategory C (id-iso-Large-Precategory C) f)
+      ( f)
+      ( left-unit-law-comp-hom-Large-Precategory C
+        ( hom-iso-Large-Precategory C f))
+
+  right-unit-law-comp-iso-Large-Precategory :
+    comp-iso-Large-Precategory C f (id-iso-Large-Precategory C) ＝ f
+  right-unit-law-comp-iso-Large-Precategory =
+    eq-iso-eq-hom-Large-Precategory C
+      ( comp-iso-Large-Precategory C f (id-iso-Large-Precategory C))
+      ( f)
+      ( right-unit-law-comp-hom-Large-Precategory C
+        ( hom-iso-Large-Precategory C f))
+```
+
+### Composition of isomorphisms is associative
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 l3 l4 : Level}
+  {X : obj-Large-Precategory C l1}
+  {Y : obj-Large-Precategory C l2}
+  {Z : obj-Large-Precategory C l3}
+  {W : obj-Large-Precategory C l4}
+  (h : iso-Large-Precategory C Z W)
+  (g : iso-Large-Precategory C Y Z)
+  (f : iso-Large-Precategory C X Y)
+  where
+
+  associative-comp-iso-Large-Precategory :
+    comp-iso-Large-Precategory C (comp-iso-Large-Precategory C h g) f ＝
+    comp-iso-Large-Precategory C h (comp-iso-Large-Precategory C g f)
+  associative-comp-iso-Large-Precategory =
+    eq-iso-eq-hom-Large-Precategory C
+      ( comp-iso-Large-Precategory C (comp-iso-Large-Precategory C h g) f)
+      ( comp-iso-Large-Precategory C h (comp-iso-Large-Precategory C g f))
+      ( associative-comp-hom-Large-Precategory C
+        ( hom-iso-Large-Precategory C h)
+        ( hom-iso-Large-Precategory C g)
+        ( hom-iso-Large-Precategory C f))
+```
+
+### Composition of isomorphisms satisfies inverse laws
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  (f : iso-Large-Precategory C X Y)
+  where
+
+  left-inverse-law-comp-iso-Large-Precategory :
+    comp-iso-Large-Precategory C (inv-iso-Large-Precategory C f) f ＝
+    id-iso-Large-Precategory C
+  left-inverse-law-comp-iso-Large-Precategory =
+    eq-iso-eq-hom-Large-Precategory C
+      ( comp-iso-Large-Precategory C (inv-iso-Large-Precategory C f) f)
+      ( id-iso-Large-Precategory C)
+      ( is-retraction-hom-inv-iso-Large-Precategory C f)
+
+  right-inverse-law-comp-iso-Large-Precategory :
+    comp-iso-Large-Precategory C f (inv-iso-Large-Precategory C f) ＝
+    id-iso-Large-Precategory C
+  right-inverse-law-comp-iso-Large-Precategory =
+    eq-iso-eq-hom-Large-Precategory C
+      ( comp-iso-Large-Precategory C f (inv-iso-Large-Precategory C f))
+      ( id-iso-Large-Precategory C)
+      ( is-section-hom-inv-iso-Large-Precategory C f)
+```
+
+### A morphism `f` is an isomorphism if and only if precomposition by `f` is an equivalence
+
+**Proof:** If `f` is an isomorphism 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 _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  {f : type-hom-Large-Precategory C X Y}
+  (H :
+    {l3 : Level} (Z : obj-Large-Precategory C l3) →
+    is-equiv (precomp-hom-Large-Precategory C f Z))
+  where
+
+  hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory :
+    type-hom-Large-Precategory C Y X
+  hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory =
+    map-inv-is-equiv (H X) (id-hom-Large-Precategory C)
+
+  is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory :
+    comp-hom-Large-Precategory C
+      ( hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory)
+      ( f) ＝
+    id-hom-Large-Precategory C
+  is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory =
+    is-section-map-inv-is-equiv (H X) (id-hom-Large-Precategory C)
+
+  is-section-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory :
+    comp-hom-Large-Precategory C
+      ( f)
+      ( hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory) ＝
+    id-hom-Large-Precategory C
+  is-section-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory =
+    is-injective-is-equiv
+      ( H Y)
+      ( ( associative-comp-hom-Large-Precategory C _ _ _) ∙
+        ( ap
+          ( comp-hom-Large-Precategory C f)
+          ( is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory)) ∙
+        ( right-unit-law-comp-hom-Large-Precategory C f) ∙
+        ( inv (left-unit-law-comp-hom-Large-Precategory C f)))
+
+  is-iso-is-equiv-precomp-hom-Large-Precategory :
+    is-iso-hom-Large-Precategory C f
+  pr1 is-iso-is-equiv-precomp-hom-Large-Precategory =
+    hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
+  pr1 (pr2 is-iso-is-equiv-precomp-hom-Large-Precategory) =
+    is-section-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
+  pr2 (pr2 is-iso-is-equiv-precomp-hom-Large-Precategory) =
+    is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
+```
+
+### A morphism `f` is an isomorphism if and only if postcomposition by `f` is an equivalence
+
+**Proof:** If `f` is an isomorphism 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 _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2}
+  {f : type-hom-Large-Precategory C X Y}
+  (H :
+    {l3 : Level} (Z : obj-Large-Precategory C l3) →
+    is-equiv (postcomp-hom-Large-Precategory C Z f))
+  where
+
+  hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory :
+    type-hom-Large-Precategory C Y X
+  hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory =
+    map-inv-is-equiv (H Y) (id-hom-Large-Precategory C)
+
+  is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory :
+    comp-hom-Large-Precategory C
+      ( f)
+      ( hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory) ＝
+    id-hom-Large-Precategory C
+  is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory =
+    is-section-map-inv-is-equiv (H Y) (id-hom-Large-Precategory C)
+
+  is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory :
+    comp-hom-Large-Precategory C
+      ( hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory)
+      ( f) ＝
+    id-hom-Large-Precategory C
+  is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory =
+    is-injective-is-equiv
+      ( H X)
+      ( ( inv (associative-comp-hom-Large-Precategory C _ _ _)) ∙
+        ( ap
+          ( comp-hom-Large-Precategory' C f)
+          ( is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory)) ∙
+        ( left-unit-law-comp-hom-Large-Precategory C f ∙
+        ( inv (right-unit-law-comp-hom-Large-Precategory C f))))
+
+  is-iso-is-equiv-postcomp-hom-Large-Precategory :
+    is-iso-hom-Large-Precategory C f
+  pr1 is-iso-is-equiv-postcomp-hom-Large-Precategory =
+    hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
+  pr1 (pr2 is-iso-is-equiv-postcomp-hom-Large-Precategory) =
+    is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
+  pr2 (pr2 is-iso-is-equiv-postcomp-hom-Large-Precategory) =
+    is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
 ```
diff --git a/src/category-theory/large-categories.lagda.md b/src/category-theory/large-categories.lagda.md
index ad3bb87709..6758ae33fe 100644
--- a/src/category-theory/large-categories.lagda.md
+++ b/src/category-theory/large-categories.lagda.md
@@ -155,6 +155,26 @@ module _
     type-hom-Large-Category Y Z →
     type-hom-Large-Category X Z
   comp-hom-Large-Category' f g = comp-hom-Large-Category g f
+
+  precomp-hom-Large-Category :
+    {l1 l2 l3 : Level}
+    {X : obj-Large-Category l1}
+    {Y : obj-Large-Category l2}
+    (f : type-hom-Large-Category X Y) →
+    (Z : obj-Large-Category l3) →
+    type-hom-Large-Category Y Z → type-hom-Large-Category X Z
+  precomp-hom-Large-Category f Z g =
+    comp-hom-Large-Category g f
+
+  postcomp-hom-Large-Category :
+    {l1 l2 l3 : Level}
+    (X : obj-Large-Category l1)
+    {Y : obj-Large-Category l2}
+    {Z : obj-Large-Category l3}
+    (f : type-hom-Large-Category Y Z) →
+    type-hom-Large-Category X Y → type-hom-Large-Category X Z
+  postcomp-hom-Large-Category X f g =
+    comp-hom-Large-Category f g
 ```
 
 ### Categories obtained from large categories
diff --git a/src/category-theory/large-precategories.lagda.md b/src/category-theory/large-precategories.lagda.md
index e5811f20ab..f128222cc7 100644
--- a/src/category-theory/large-precategories.lagda.md
+++ b/src/category-theory/large-precategories.lagda.md
@@ -119,6 +119,26 @@ module _
     type-hom-Large-Precategory Y Z →
     type-hom-Large-Precategory X Z
   comp-hom-Large-Precategory' f g = comp-hom-Large-Precategory C g f
+
+  precomp-hom-Large-Precategory :
+    {l1 l2 l3 : Level}
+    {X : obj-Large-Precategory C l1}
+    {Y : obj-Large-Precategory C l2}
+    (f : type-hom-Large-Precategory X Y) →
+    (Z : obj-Large-Precategory C l3) →
+    type-hom-Large-Precategory Y Z → type-hom-Large-Precategory X Z
+  precomp-hom-Large-Precategory f Z g =
+    comp-hom-Large-Precategory C g f
+
+  postcomp-hom-Large-Precategory :
+    {l1 l2 l3 : Level}
+    (X : obj-Large-Precategory C l1)
+    {Y : obj-Large-Precategory C l2}
+    {Z : obj-Large-Precategory C l3}
+    (f : type-hom-Large-Precategory Y Z) →
+    type-hom-Large-Precategory X Y → type-hom-Large-Precategory X Z
+  postcomp-hom-Large-Precategory X f g =
+    comp-hom-Large-Precategory C f g
 ```
 
 ### Precategories obtained from large precategories
diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
index b90484ca8a..043c3a13b4 100644
--- a/src/category-theory/monomorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
@@ -64,7 +64,7 @@ module _
   where
 
   is-mono-iso-Large-Precategory :
-    is-mono-Large-Precategory C l3 X Y (hom-iso-Large-Precategory C X Y f)
+    is-mono-Large-Precategory C l3 X Y (hom-iso-Large-Precategory C f)
   is-mono-iso-Large-Precategory Z g h =
     is-equiv-is-invertible
       ( λ P →
@@ -72,32 +72,32 @@ module _
           ( left-unit-law-comp-hom-Large-Precategory C g)) ∙
           ( ( ap
             ( λ h' → comp-hom-Large-Precategory C h' g)
-            ( inv (is-retraction-hom-inv-iso-Large-Precategory C X Y f))) ∙
+            ( inv (is-retraction-hom-inv-iso-Large-Precategory C f))) ∙
             ( ( associative-comp-hom-Large-Precategory C
-              ( hom-inv-iso-Large-Precategory C X Y f)
-              ( hom-iso-Large-Precategory C X Y f)
+              ( hom-inv-iso-Large-Precategory C f)
+              ( hom-iso-Large-Precategory C f)
               ( g)) ∙
               ( ( ap
                 ( comp-hom-Large-Precategory C
-                  ( hom-inv-iso-Large-Precategory C X Y f))
+                  ( hom-inv-iso-Large-Precategory C f))
                 ( P)) ∙
                 ( ( inv
                   ( associative-comp-hom-Large-Precategory C
-                    ( hom-inv-iso-Large-Precategory C X Y f)
-                    ( hom-iso-Large-Precategory C X Y f)
+                    ( hom-inv-iso-Large-Precategory C f)
+                    ( hom-iso-Large-Precategory C f)
                     ( h))) ∙
                   ( ( ap
                     ( λ h' → comp-hom-Large-Precategory C h' h)
-                    ( is-retraction-hom-inv-iso-Large-Precategory C X Y f)) ∙
+                    ( is-retraction-hom-inv-iso-Large-Precategory C f)) ∙
                     ( left-unit-law-comp-hom-Large-Precategory C h)))))))
       ( λ p →
         eq-is-prop
           ( is-set-type-hom-Large-Precategory C Z Y
             ( comp-hom-Large-Precategory C
-              ( hom-iso-Large-Precategory C X Y f)
+              ( hom-iso-Large-Precategory C f)
               ( g))
             ( comp-hom-Large-Precategory C
-              ( hom-iso-Large-Precategory C X Y f)
+              ( hom-iso-Large-Precategory C f)
               ( h))))
       ( λ p → eq-is-prop (is-set-type-hom-Large-Precategory C Z X g h))
 ```
diff --git a/src/category-theory/natural-isomorphisms-large-precategories.lagda.md b/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
index 2c637856e2..907bb4df14 100644
--- a/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
@@ -49,14 +49,10 @@ module _
         ( f : type-hom-Large-Precategory C X Y) →
         square-Large-Precategory D
           ( hom-iso-Large-Precategory D
-            ( obj-functor-Large-Precategory F X)
-            ( obj-functor-Large-Precategory G X)
             ( obj-natural-isomorphism-Large-Precategory X))
           ( hom-functor-Large-Precategory F f)
           ( hom-functor-Large-Precategory G f)
           ( hom-iso-Large-Precategory D
-            ( obj-functor-Large-Precategory F Y)
-            ( obj-functor-Large-Precategory G Y)
             ( obj-natural-isomorphism-Large-Precategory Y))
 
   open natural-isomorphism-Large-Precategory public
@@ -67,8 +63,6 @@ module _
   obj-natural-transformation-Large-Precategory
     ( natural-transformation-natural-isomorphism-Large-Precategory γ) X =
     hom-iso-Large-Precategory D
-      ( obj-functor-Large-Precategory F X)
-      ( obj-functor-Large-Precategory G X)
       ( obj-natural-isomorphism-Large-Precategory γ X)
   coherence-square-natural-transformation-Large-Precategory
     (natural-transformation-natural-isomorphism-Large-Precategory γ) =
diff --git a/src/group-theory/isomorphisms-group-actions.lagda.md b/src/group-theory/isomorphisms-group-actions.lagda.md
index 90f3c08064..2102bfff9c 100644
--- a/src/group-theory/isomorphisms-group-actions.lagda.md
+++ b/src/group-theory/isomorphisms-group-actions.lagda.md
@@ -45,7 +45,7 @@ module _
 
   hom-iso-Abstract-Group-Action :
     type-iso-Abstract-Group-Action → type-hom-Abstract-Group-Action G X Y
-  hom-iso-Abstract-Group-Action = hom-iso-Large-Precategory C X Y
+  hom-iso-Abstract-Group-Action = hom-iso-Large-Precategory C {X = X} {Y = Y}
 
   map-iso-Abstract-Group-Action :
     type-iso-Abstract-Group-Action →
@@ -66,7 +66,8 @@ module _
 
   hom-inv-iso-Abstract-Group-Action :
     type-iso-Abstract-Group-Action → type-hom-Abstract-Group-Action G Y X
-  hom-inv-iso-Abstract-Group-Action = hom-inv-iso-Large-Precategory C X Y
+  hom-inv-iso-Abstract-Group-Action =
+    hom-inv-iso-Large-Precategory C {X = X} {Y = Y}
 
   map-hom-inv-iso-Abstract-Group-Action :
     type-iso-Abstract-Group-Action →
@@ -83,7 +84,7 @@ module _
         ( hom-inv-iso-Abstract-Group-Action f))
       ( id-hom-Abstract-Group-Action G Y)
   is-section-hom-inv-iso-Abstract-Group-Action =
-    is-section-hom-inv-iso-Large-Precategory C X Y
+    is-section-hom-inv-iso-Large-Precategory C {X = X} {Y = Y}
 
   is-retraction-hom-inv-iso-Abstract-Group-Action :
     (f : type-iso-Abstract-Group-Action) →
@@ -93,12 +94,13 @@ module _
         ( hom-iso-Abstract-Group-Action f))
       ( id-hom-Abstract-Group-Action G X)
   is-retraction-hom-inv-iso-Abstract-Group-Action =
-    is-retraction-hom-inv-iso-Large-Precategory C X Y
+    is-retraction-hom-inv-iso-Large-Precategory C {X = X} {Y = Y}
 
   is-iso-iso-Abstract-Group-Action :
     (f : type-iso-Abstract-Group-Action) →
     is-iso-hom-Abstract-Group-Action (hom-iso-Abstract-Group-Action f)
-  is-iso-iso-Abstract-Group-Action = is-iso-iso-Large-Precategory C X Y
+  is-iso-iso-Abstract-Group-Action =
+    is-iso-iso-Large-Precategory C {X = X} {Y = Y}
 
   equiv-iso-Abstract-Group-Action :
     type-iso-Abstract-Group-Action → equiv-Abstract-Group-Action G X Y
diff --git a/src/group-theory/isomorphisms-groups.lagda.md b/src/group-theory/isomorphisms-groups.lagda.md
index 3076f52f36..dfd47296a8 100644
--- a/src/group-theory/isomorphisms-groups.lagda.md
+++ b/src/group-theory/isomorphisms-groups.lagda.md
@@ -255,7 +255,8 @@ module _
 
   comp-iso-Group :
     type-iso-Group H K → type-iso-Group G H → type-iso-Group G K
-  comp-iso-Group = comp-iso-Large-Precategory Group-Large-Precategory G H K
+  comp-iso-Group =
+    comp-iso-Large-Precategory Group-Large-Precategory {X = G} {Y = H} {Z = K}
 ```
 
 ### Group isomorphisms are stable by inversion
@@ -266,5 +267,6 @@ module _
   where
 
   inv-iso-Group : type-iso-Group G H → type-iso-Group H G
-  inv-iso-Group = inv-iso-Large-Precategory Group-Large-Precategory G H
+  inv-iso-Group =
+    inv-iso-Large-Precategory Group-Large-Precategory {X = G} {Y = H}
 ```
diff --git a/src/group-theory/isomorphisms-semigroups.lagda.md b/src/group-theory/isomorphisms-semigroups.lagda.md
index 58f154ce6e..a2014912ad 100644
--- a/src/group-theory/isomorphisms-semigroups.lagda.md
+++ b/src/group-theory/isomorphisms-semigroups.lagda.md
@@ -116,7 +116,8 @@ module _
   type-iso-Semigroup = iso-Large-Precategory Semigroup-Large-Precategory G H
 
   hom-iso-Semigroup : type-iso-Semigroup → type-hom-Semigroup G H
-  hom-iso-Semigroup = hom-iso-Large-Precategory Semigroup-Large-Precategory G H
+  hom-iso-Semigroup =
+    hom-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H}
 
   map-iso-Semigroup : type-iso-Semigroup → type-Semigroup G → type-Semigroup H
   map-iso-Semigroup f = map-hom-Semigroup G H (hom-iso-Semigroup f)
@@ -131,11 +132,11 @@ module _
   is-iso-iso-Semigroup :
     (f : type-iso-Semigroup) → is-iso-hom-Semigroup G H (hom-iso-Semigroup f)
   is-iso-iso-Semigroup =
-    is-iso-iso-Large-Precategory Semigroup-Large-Precategory G H
+    is-iso-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H}
 
   hom-inv-iso-Semigroup : type-iso-Semigroup → type-hom-Semigroup H G
   hom-inv-iso-Semigroup =
-    hom-inv-iso-Large-Precategory Semigroup-Large-Precategory G H
+    hom-inv-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H}
 
   map-inv-iso-Semigroup :
     type-iso-Semigroup → type-Semigroup H → type-Semigroup G
@@ -154,7 +155,10 @@ module _
     comp-hom-Semigroup H G H (hom-iso-Semigroup f) (hom-inv-iso-Semigroup f) ＝
     id-hom-Semigroup H
   is-section-hom-inv-iso-Semigroup =
-    is-section-hom-inv-iso-Large-Precategory Semigroup-Large-Precategory G H
+    is-section-hom-inv-iso-Large-Precategory
+      ( Semigroup-Large-Precategory)
+      { X = G}
+      { Y = H}
 
   is-section-map-inv-iso-Semigroup :
     (f : type-iso-Semigroup) →
@@ -172,7 +176,10 @@ module _
     comp-hom-Semigroup G H G (hom-inv-iso-Semigroup f) (hom-iso-Semigroup f) ＝
     id-hom-Semigroup G
   is-retraction-hom-inv-iso-Semigroup =
-    is-retraction-hom-inv-iso-Large-Precategory Semigroup-Large-Precategory G H
+    is-retraction-hom-inv-iso-Large-Precategory
+      ( Semigroup-Large-Precategory)
+      { X = G}
+      { Y = H}
 
   is-retraction-map-inv-iso-Semigroup :
     (f : type-iso-Semigroup) →
@@ -199,12 +206,18 @@ module _
     is-prop-is-iso-hom-Semigroup :
       (f : type-hom-Semigroup G H) → is-prop (is-iso-hom-Semigroup G H f)
     is-prop-is-iso-hom-Semigroup =
-      is-prop-is-iso-hom-Large-Precategory Semigroup-Large-Precategory G H
+      is-prop-is-iso-hom-Large-Precategory
+        ( Semigroup-Large-Precategory)
+        { X = G}
+        { Y = H}
 
   is-iso-prop-hom-Semigroup :
     type-hom-Semigroup G H → Prop (l1 ⊔ l2)
   is-iso-prop-hom-Semigroup =
-    is-iso-prop-hom-Large-Precategory Semigroup-Large-Precategory G H
+    is-iso-prop-hom-Large-Precategory
+      ( Semigroup-Large-Precategory)
+      { X = G}
+      { Y = H}
 ```
 
 ### The inverse of an equivalence of semigroups preserves the binary operation
diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md
index 17a9a73284..706ee3c40c 100644
--- a/src/ring-theory/isomorphisms-rings.lagda.md
+++ b/src/ring-theory/isomorphisms-rings.lagda.md
@@ -49,7 +49,7 @@ module _
 
   is-iso-prop-hom-Ring : Prop (l1 ⊔ l2)
   is-iso-prop-hom-Ring =
-    is-iso-prop-hom-Large-Precategory Ring-Large-Precategory R S f
+    is-iso-prop-hom-Large-Precategory Ring-Large-Precategory {X = R} {Y = S} f
 
   is-iso-hom-Ring : UU (l1 ⊔ l2)
   is-iso-hom-Ring =
@@ -57,7 +57,11 @@ module _
 
   is-prop-is-iso-hom-Ring : is-prop is-iso-hom-Ring
   is-prop-is-iso-hom-Ring =
-    is-prop-is-iso-hom-Large-Precategory Ring-Large-Precategory R S f
+    is-prop-is-iso-hom-Large-Precategory
+      ( Ring-Large-Precategory)
+      { X = R}
+      { Y = S}
+      ( f)
 
   hom-inv-is-iso-hom-Ring : is-iso-hom-Ring → type-hom-Ring S R
   hom-inv-is-iso-hom-Ring =
@@ -119,7 +123,8 @@ module _
   iso-Ring = iso-Large-Precategory Ring-Large-Precategory R S
 
   hom-iso-Ring : iso-Ring → type-hom-Ring R S
-  hom-iso-Ring = hom-iso-Large-Precategory Ring-Large-Precategory R S
+  hom-iso-Ring =
+    hom-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S}
 
   map-iso-Ring : iso-Ring → type-Ring R → type-Ring S
   map-iso-Ring f = map-hom-Ring R S (hom-iso-Ring f)
@@ -153,11 +158,11 @@ module _
   is-iso-iso-Ring :
     (f : iso-Ring) → is-iso-hom-Ring R S (hom-iso-Ring f)
   is-iso-iso-Ring =
-    is-iso-iso-Large-Precategory Ring-Large-Precategory R S
+    is-iso-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S}
 
   hom-inv-iso-Ring : iso-Ring → type-hom-Ring S R
   hom-inv-iso-Ring =
-    hom-inv-iso-Large-Precategory Ring-Large-Precategory R S
+    hom-inv-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S}
 
   map-inv-iso-Ring : iso-Ring → type-Ring S → type-Ring R
   map-inv-iso-Ring f = map-hom-Ring S R (hom-inv-iso-Ring f)
@@ -196,7 +201,10 @@ module _
     (f : iso-Ring) →
     comp-hom-Ring S R S (hom-iso-Ring f) (hom-inv-iso-Ring f) ＝ id-hom-Ring S
   is-section-hom-inv-iso-Ring =
-    is-section-hom-inv-iso-Large-Precategory Ring-Large-Precategory R S
+    is-section-hom-inv-iso-Large-Precategory
+      ( Ring-Large-Precategory)
+      { X = R}
+      { Y = S}
 
   is-section-map-inv-iso-Ring :
     (f : iso-Ring) → map-iso-Ring f ∘ map-inv-iso-Ring f ~ id
@@ -210,7 +218,10 @@ module _
     (f : iso-Ring) →
     comp-hom-Ring R S R (hom-inv-iso-Ring f) (hom-iso-Ring f) ＝ id-hom-Ring R
   is-retraction-hom-inv-iso-Ring =
-    is-retraction-hom-inv-iso-Large-Precategory Ring-Large-Precategory R S
+    is-retraction-hom-inv-iso-Large-Precategory
+      ( Ring-Large-Precategory)
+      { X = R}
+      { Y = S}
 
   is-retraction-map-inv-iso-Ring :
     (f : iso-Ring) → map-inv-iso-Ring f ∘ map-iso-Ring f ~ id