From 65483f602e297fc65ea2e174bf8ea9b1ab16f88c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 19 Sep 2023 02:25:24 +0200
Subject: [PATCH] `comp-natural-transformation-Large-Precategory` and
 associated refactoring

---
 .../adjunctions-large-precategories.lagda.md  | 595 ++++++++++--------
 .../functors-categories.lagda.md              |   4 +-
 .../functors-large-precategories.lagda.md     |   3 +-
 ...ansformations-large-precategories.lagda.md |   4 +-
 .../natural-isomorphisms-categories.lagda.md  |   8 +
 ...-isomorphisms-large-precategories.lagda.md |  39 +-
 ...atural-isomorphisms-precategories.lagda.md |  17 +-
 ...atural-transformations-categories.lagda.md |  35 +-
 ...ansformations-large-precategories.lagda.md |  70 ++-
 ...ral-transformations-precategories.lagda.md |  38 +-
 10 files changed, 484 insertions(+), 329 deletions(-)

diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
index 9a1a907824..cda2dab0a7 100644
--- a/src/category-theory/adjunctions-large-precategories.lagda.md
+++ b/src/category-theory/adjunctions-large-precategories.lagda.md
@@ -22,10 +22,13 @@ open import foundation.universe-levels
 
 ## Idea
 
-Let `C` and `D` be two large precategories. Two functors `F : C → D` and
-`G : D → C` constitute an adjoint pair if
+Let `C` and `D` be two
+[large precategories](category-theory.large-precategories.md). Two
+[functors](category-theory.functors-large-precategories.md) `F : C → D` and
+`G : D → C` constitute an **adjoint pair** if
 
-- for each pair of objects `X` in `C` and `Y` in `D`, there is an equivalence
+- for each pair of objects `X` in `C` and `Y` in `D`, there is an
+  [equivalence](foundation-core.equivalences.md)
   `ϕ X Y : hom X (G Y) ≃ hom (F X) Y` such that
 - for every pair of morhpisms `f : X₂ → X₁` and `g : Y₁ → Y₂` the following
   square commutes:
@@ -41,16 +44,19 @@ G g ∘ _ ∘ f |                        | g ∘ _ ∘ F f
                        ϕ X₂ Y₂
 ```
 
-In this case we say that `F` is left adjoint to `G` and `G` is right adjoint to
-`F` and write this as `F ⊣ G`.
+In this case we say that `F` is **left adjoint** to `G` and `G` is **right
+adjoint** to `F` and write this as `F ⊣ G`.
 
 ## Definition
 
 ```agda
 module _
-  {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level}
-  {C : Large-Precategory αC βC} {D : Large-Precategory αD βD}
-  (F : functor-Large-Precategory C D γF) (G : functor-Large-Precategory D C γG)
+  {αC αD γF γG : Level → Level}
+  {βC βD : Level → Level → Level}
+  {C : Large-Precategory αC βC}
+  {D : Large-Precategory αD βD}
+  (F : functor-Large-Precategory C D γF)
+  (G : functor-Large-Precategory D C γG)
   where
 
   record is-adjoint-pair-Large-Precategory : UUω
@@ -67,8 +73,10 @@ module _
           ( Y))
       naturality-equiv-is-adjoint-pair-Large-Precategory :
         { l1 l2 l3 l4 : Level}
-        { X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2}
-        { Y1 : obj-Large-Precategory D l3} {Y2 : obj-Large-Precategory D l4}
+        { X1 : obj-Large-Precategory C l1}
+        { X2 : obj-Large-Precategory C l2}
+        { Y1 : obj-Large-Precategory D l3}
+        { Y2 : obj-Large-Precategory D l4}
         ( f : type-hom-Large-Precategory C X2 X1)
         ( g : type-hom-Large-Precategory D Y1 Y2) →
         coherence-square-maps
@@ -76,7 +84,8 @@ module _
           ( λ h →
             comp-hom-Large-Precategory C
               ( comp-hom-Large-Precategory C
-                ( map-hom-functor-Large-Precategory G g) h)
+                ( map-hom-functor-Large-Precategory G g)
+                ( h))
               ( f))
           ( λ h →
             comp-hom-Large-Precategory D
@@ -95,8 +104,10 @@ module _
     map-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)
 
   inv-equiv-is-adjoint-pair-Large-Precategory :
-    (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
-    (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
+    (H : is-adjoint-pair-Large-Precategory)
+    {l1 l2 : Level}
+    (X : obj-Large-Precategory C l1)
+    (Y : obj-Large-Precategory D l2) →
     ( type-hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y) ≃
     ( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y))
   inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
@@ -104,7 +115,8 @@ module _
 
   map-inv-equiv-is-adjoint-pair-Large-Precategory :
     (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
-    (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
+    (X : obj-Large-Precategory C l1)
+    (Y : obj-Large-Precategory D l2) →
     ( type-hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y) →
     ( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y))
   map-inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
@@ -113,8 +125,10 @@ module _
   naturality-inv-equiv-is-adjoint-pair-Large-Precategory :
     ( H : is-adjoint-pair-Large-Precategory)
     { l1 l2 l3 l4 : Level}
-    { X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2}
-    { Y1 : obj-Large-Precategory D l3} {Y2 : obj-Large-Precategory D l4}
+    { X1 : obj-Large-Precategory C l1}
+    { X2 : obj-Large-Precategory C l2}
+    { Y1 : obj-Large-Precategory D l3}
+    { Y2 : obj-Large-Precategory D l4}
     ( f : type-hom-Large-Precategory C X2 X1)
     ( g : type-hom-Large-Precategory D Y1 Y2) →
     coherence-square-maps
@@ -148,9 +162,12 @@ module _
       ( naturality-equiv-is-adjoint-pair-Large-Precategory H f g)
 
 module _
-  {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level}
-  {C : Large-Precategory αC βC} {D : Large-Precategory αD βD}
-  (G : functor-Large-Precategory D C γG) (F : functor-Large-Precategory C D γF)
+  {αC αD γF γG : Level → Level}
+  {βC βD : Level → Level → Level}
+  {C : Large-Precategory αC βC}
+  {D : Large-Precategory αD βD}
+  (G : functor-Large-Precategory D C γG)
+  (F : functor-Large-Precategory C D γF)
   where
 
   is-left-adjoint-functor-Large-Precategory : UUω
@@ -158,9 +175,12 @@ module _
     is-adjoint-pair-Large-Precategory F G
 
 module _
-  {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level}
-  {C : Large-Precategory αC βC} {D : Large-Precategory αD βD}
-  (F : functor-Large-Precategory C D γF) (G : functor-Large-Precategory D C γG)
+  {αC αD γF γG : Level → Level}
+  {βC βD : Level → Level → Level}
+  {C : Large-Precategory αC βC}
+  {D : Large-Precategory αD βD}
+  (F : functor-Large-Precategory C D γF)
+  (G : functor-Large-Precategory D C γG)
   where
 
   is-right-adjoint-functor-Large-Precategory : UUω
@@ -168,153 +188,211 @@ module _
     is-adjoint-pair-Large-Precategory F G
 
 module _
-  {αC αD : Level → Level} {βC βD : Level → Level → Level}
-  (C : Large-Precategory αC βC) (D : Large-Precategory αD βD)
+  {αC αD : Level → Level}
+  {βC βD : Level → Level → Level}
+  (C : Large-Precategory αC βC)
+  (D : Large-Precategory αD βD)
   where
 
-  record Adjunction : UUω where
+  record Adjunction-Large-Precategory : UUω where
     field
-      level-left-adjoint-Adjunction :
+      level-left-adjoint-Adjunction-Large-Precategory :
         Level → Level
-      left-adjoint-Adjunction :
-        functor-Large-Precategory C D level-left-adjoint-Adjunction
-      level-right-adjoint-Adjunction :
+      left-adjoint-Adjunction-Large-Precategory :
+        functor-Large-Precategory C D
+          level-left-adjoint-Adjunction-Large-Precategory
+      level-right-adjoint-Adjunction-Large-Precategory :
         Level → Level
-      right-adjoint-Adjunction :
-        functor-Large-Precategory D C level-right-adjoint-Adjunction
-      is-adjoint-pair-Adjunction :
+      right-adjoint-Adjunction-Large-Precategory :
+        functor-Large-Precategory D C
+          level-right-adjoint-Adjunction-Large-Precategory
+      is-adjoint-pair-Adjunction-Large-Precategory :
         is-adjoint-pair-Large-Precategory
-          left-adjoint-Adjunction
-          right-adjoint-Adjunction
+          left-adjoint-Adjunction-Large-Precategory
+          right-adjoint-Adjunction-Large-Precategory
 
-  open Adjunction public
+  open Adjunction-Large-Precategory public
 
-  obj-left-adjoint-Adjunction :
-    (FG : Adjunction) {l : Level} →
+  obj-left-adjoint-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory) {l : Level} →
     obj-Large-Precategory C l →
-    obj-Large-Precategory D (level-left-adjoint-Adjunction FG l)
-  obj-left-adjoint-Adjunction FG =
-    map-obj-functor-Large-Precategory (left-adjoint-Adjunction FG)
-
-  hom-left-adjoint-Adjunction :
-    (FG : Adjunction) {l1 l2 : Level}
-    {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} →
+    obj-Large-Precategory D
+      ( level-left-adjoint-Adjunction-Large-Precategory FG l)
+  obj-left-adjoint-Adjunction-Large-Precategory FG =
+    map-obj-functor-Large-Precategory
+      ( left-adjoint-Adjunction-Large-Precategory FG)
+
+  hom-left-adjoint-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 : Level}
+    {X : obj-Large-Precategory C l1}
+    {Y : obj-Large-Precategory C l2} →
     type-hom-Large-Precategory C X Y →
     type-hom-Large-Precategory D
-      ( obj-left-adjoint-Adjunction FG X)
-      ( obj-left-adjoint-Adjunction FG Y)
-  hom-left-adjoint-Adjunction FG =
-    map-hom-functor-Large-Precategory (left-adjoint-Adjunction FG)
-
-  preserves-id-left-adjoint-Adjunction :
-    (FG : Adjunction) {l1 : Level} (X : obj-Large-Precategory C l1) →
-    ( hom-left-adjoint-Adjunction FG (id-hom-Large-Precategory C {X = X})) ＝
+      ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
+      ( obj-left-adjoint-Adjunction-Large-Precategory FG Y)
+  hom-left-adjoint-Adjunction-Large-Precategory FG =
+    map-hom-functor-Large-Precategory
+      ( left-adjoint-Adjunction-Large-Precategory FG)
+
+  preserves-id-left-adjoint-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 : Level}
+    (X : obj-Large-Precategory C l1) →
+    ( hom-left-adjoint-Adjunction-Large-Precategory FG
+      ( id-hom-Large-Precategory C {X = X})) ＝
     ( id-hom-Large-Precategory D)
-  preserves-id-left-adjoint-Adjunction FG X =
-    preserves-id-functor-Large-Precategory (left-adjoint-Adjunction FG)
+  preserves-id-left-adjoint-Adjunction-Large-Precategory FG X =
+    preserves-id-functor-Large-Precategory
+      ( left-adjoint-Adjunction-Large-Precategory FG)
 
-  obj-right-adjoint-Adjunction :
-    (FG : Adjunction) {l1 : Level} →
+  obj-right-adjoint-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 : Level} →
     obj-Large-Precategory D l1 →
-    obj-Large-Precategory C (level-right-adjoint-Adjunction FG l1)
-  obj-right-adjoint-Adjunction FG =
-    map-obj-functor-Large-Precategory (right-adjoint-Adjunction FG)
-
-  hom-right-adjoint-Adjunction :
-    (FG : Adjunction) {l1 l2 : Level} {X : obj-Large-Precategory D l1}
+    obj-Large-Precategory C
+      ( level-right-adjoint-Adjunction-Large-Precategory FG l1)
+  obj-right-adjoint-Adjunction-Large-Precategory FG =
+    map-obj-functor-Large-Precategory
+      ( right-adjoint-Adjunction-Large-Precategory FG)
+
+  hom-right-adjoint-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 : Level}
+    {X : obj-Large-Precategory D l1}
     {Y : obj-Large-Precategory D l2} →
     type-hom-Large-Precategory D X Y →
     type-hom-Large-Precategory C
-      ( obj-right-adjoint-Adjunction FG X)
-      ( obj-right-adjoint-Adjunction FG Y)
-  hom-right-adjoint-Adjunction FG =
-    map-hom-functor-Large-Precategory (right-adjoint-Adjunction FG)
-
-  preserves-id-right-adjoint-Adjunction :
-    (FG : Adjunction) {l : Level} (Y : obj-Large-Precategory D l) →
-    ( hom-right-adjoint-Adjunction FG (id-hom-Large-Precategory D {X = Y})) ＝
+      ( obj-right-adjoint-Adjunction-Large-Precategory FG X)
+      ( obj-right-adjoint-Adjunction-Large-Precategory FG Y)
+  hom-right-adjoint-Adjunction-Large-Precategory FG =
+    map-hom-functor-Large-Precategory
+      ( right-adjoint-Adjunction-Large-Precategory FG)
+
+  preserves-id-right-adjoint-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l : Level}
+    (Y : obj-Large-Precategory D l) →
+    ( hom-right-adjoint-Adjunction-Large-Precategory FG
+      ( id-hom-Large-Precategory D {X = Y})) ＝
     ( id-hom-Large-Precategory C)
-  preserves-id-right-adjoint-Adjunction FG Y =
-    preserves-id-functor-Large-Precategory (right-adjoint-Adjunction FG)
-
-  equiv-is-adjoint-pair-Adjunction :
-    (FG : Adjunction) {l1 l2 : Level} (X : obj-Large-Precategory C l1)
+  preserves-id-right-adjoint-Adjunction-Large-Precategory FG Y =
+    preserves-id-functor-Large-Precategory
+      ( right-adjoint-Adjunction-Large-Precategory FG)
+
+  equiv-is-adjoint-pair-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 : Level}
+    (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory C X (obj-right-adjoint-Adjunction FG Y) ≃
-    type-hom-Large-Precategory D (obj-left-adjoint-Adjunction FG X) Y
-  equiv-is-adjoint-pair-Adjunction FG =
-    equiv-is-adjoint-pair-Large-Precategory (is-adjoint-pair-Adjunction FG)
-
-  map-equiv-is-adjoint-pair-Adjunction :
-    (FG : Adjunction) {l1 l2 : Level} (X : obj-Large-Precategory C l1)
+    type-hom-Large-Precategory C
+      ( X)
+      ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) ≃
+    type-hom-Large-Precategory D
+      ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
+      ( Y)
+  equiv-is-adjoint-pair-Adjunction-Large-Precategory FG =
+    equiv-is-adjoint-pair-Large-Precategory
+      ( is-adjoint-pair-Adjunction-Large-Precategory FG)
+
+  map-equiv-is-adjoint-pair-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 : Level}
+    (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory C X (obj-right-adjoint-Adjunction FG Y) →
-    type-hom-Large-Precategory D (obj-left-adjoint-Adjunction FG X) Y
-  map-equiv-is-adjoint-pair-Adjunction FG =
+    type-hom-Large-Precategory C
+      ( X)
+      ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) →
+    type-hom-Large-Precategory D
+      ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
+      ( Y)
+  map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG =
     map-equiv-is-adjoint-pair-Large-Precategory
-      ( left-adjoint-Adjunction FG)
-      ( right-adjoint-Adjunction FG)
-      ( is-adjoint-pair-Adjunction FG)
-
-  naturality-equiv-is-adjoint-pair-Adjunction :
-    (FG : Adjunction) {l1 l2 l3 l4 : Level}
-    {X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2}
-    {Y1 : obj-Large-Precategory D l3} {Y2 : obj-Large-Precategory D l4}
+      ( left-adjoint-Adjunction-Large-Precategory FG)
+      ( right-adjoint-Adjunction-Large-Precategory FG)
+      ( is-adjoint-pair-Adjunction-Large-Precategory FG)
+
+  naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 l3 l4 : Level}
+    {X1 : obj-Large-Precategory C l1}
+    {X2 : obj-Large-Precategory C l2}
+    {Y1 : obj-Large-Precategory D l3}
+    {Y2 : obj-Large-Precategory D l4}
     (f : type-hom-Large-Precategory C X2 X1)
     (g : type-hom-Large-Precategory D Y1 Y2) →
     coherence-square-maps
-      ( map-equiv-is-adjoint-pair-Adjunction FG X1 Y1)
+      ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1)
       ( λ h →
         comp-hom-Large-Precategory C
-          ( comp-hom-Large-Precategory C (hom-right-adjoint-Adjunction FG g) h)
+          ( comp-hom-Large-Precategory C
+            ( hom-right-adjoint-Adjunction-Large-Precategory FG g)
+            ( h))
           ( f))
       ( λ h →
         comp-hom-Large-Precategory D
           ( comp-hom-Large-Precategory D g h)
-          ( hom-left-adjoint-Adjunction FG f))
-      ( map-equiv-is-adjoint-pair-Adjunction FG X2 Y2)
-  naturality-equiv-is-adjoint-pair-Adjunction FG =
+          ( hom-left-adjoint-Adjunction-Large-Precategory FG f))
+      ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X2 Y2)
+  naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG =
     naturality-equiv-is-adjoint-pair-Large-Precategory
-      ( is-adjoint-pair-Adjunction FG)
+      ( is-adjoint-pair-Adjunction-Large-Precategory FG)
 
-  inv-equiv-is-adjoint-pair-Adjunction :
-    (FG : Adjunction) {l1 l2 : Level} (X : obj-Large-Precategory C l1)
+  inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 : Level}
+    (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory D (obj-left-adjoint-Adjunction FG X) Y ≃
-    type-hom-Large-Precategory C X (obj-right-adjoint-Adjunction FG Y)
-  inv-equiv-is-adjoint-pair-Adjunction FG X Y =
-    inv-equiv (equiv-is-adjoint-pair-Adjunction FG X Y)
-
-  map-inv-equiv-is-adjoint-pair-Adjunction :
-    (FG : Adjunction) {l1 l2 : Level} (X : obj-Large-Precategory C l1)
+    ( type-hom-Large-Precategory D
+      ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
+      ( Y)) ≃
+    ( type-hom-Large-Precategory C
+      ( X)
+      ( obj-right-adjoint-Adjunction-Large-Precategory FG Y))
+  inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y =
+    inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y)
+
+  map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 : Level}
+    (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory D (obj-left-adjoint-Adjunction FG X) Y →
-    type-hom-Large-Precategory C X (obj-right-adjoint-Adjunction FG Y)
-  map-inv-equiv-is-adjoint-pair-Adjunction FG X Y =
-    map-inv-equiv (equiv-is-adjoint-pair-Adjunction FG X Y)
-
-  naturality-inv-equiv-is-adjoint-pair-Adjunction :
-    (FG : Adjunction) {l1 l2 l3 l4 : Level}
-    {X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2}
-    {Y1 : obj-Large-Precategory D l3} {Y2 : obj-Large-Precategory D l4}
+    type-hom-Large-Precategory D
+      ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
+      ( Y) →
+    type-hom-Large-Precategory C
+      ( X)
+      ( obj-right-adjoint-Adjunction-Large-Precategory FG Y)
+  map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y =
+    map-inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y)
+
+  naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory)
+    {l1 l2 l3 l4 : Level}
+    {X1 : obj-Large-Precategory C l1}
+    {X2 : obj-Large-Precategory C l2}
+    {Y1 : obj-Large-Precategory D l3}
+    {Y2 : obj-Large-Precategory D l4}
     (f : type-hom-Large-Precategory C X2 X1)
     (g : type-hom-Large-Precategory D Y1 Y2) →
     coherence-square-maps
-      ( map-inv-equiv-is-adjoint-pair-Adjunction FG X1 Y1)
+      ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1)
       ( λ h →
         comp-hom-Large-Precategory D
           ( comp-hom-Large-Precategory D g h)
-          ( hom-left-adjoint-Adjunction FG f))
+          ( hom-left-adjoint-Adjunction-Large-Precategory FG f))
       ( λ h →
         comp-hom-Large-Precategory C
-          ( comp-hom-Large-Precategory C (hom-right-adjoint-Adjunction FG g) h)
+          ( comp-hom-Large-Precategory C
+            ( hom-right-adjoint-Adjunction-Large-Precategory FG g)
+            ( h))
           ( f))
-      ( map-inv-equiv-is-adjoint-pair-Adjunction FG X2 Y2)
-  naturality-inv-equiv-is-adjoint-pair-Adjunction FG =
+      ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X2 Y2)
+  naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG =
     naturality-inv-equiv-is-adjoint-pair-Large-Precategory
-      ( left-adjoint-Adjunction FG)
-      ( right-adjoint-Adjunction FG)
-      ( is-adjoint-pair-Adjunction FG)
+      ( left-adjoint-Adjunction-Large-Precategory FG)
+      ( right-adjoint-Adjunction-Large-Precategory FG)
+      ( is-adjoint-pair-Adjunction-Large-Precategory FG)
 ```
 
 ## Properties
@@ -330,85 +408,93 @@ module _
   (C : Large-Precategory αC βC) (D : Large-Precategory αD βD)
   where
 
-  unit-Adjunction :
-    (FG : Adjunction C D) →
+  unit-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory C D) →
     natural-transformation-Large-Precategory
       ( id-functor-Large-Precategory)
       ( comp-functor-Large-Precategory
-        ( right-adjoint-Adjunction FG)
-        ( left-adjoint-Adjunction FG))
-  obj-natural-transformation-Large-Precategory (unit-Adjunction FG) X =
-    map-inv-equiv-is-adjoint-pair-Adjunction C D FG X
-      ( obj-left-adjoint-Adjunction C D FG X)
+        ( right-adjoint-Adjunction-Large-Precategory FG)
+        ( left-adjoint-Adjunction-Large-Precategory FG))
+  components-natural-transformation-Large-Precategory
+    ( unit-Adjunction-Large-Precategory FG)
+    ( X) =
+    map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG X
+      ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X)
       ( id-hom-Large-Precategory D)
   coherence-square-natural-transformation-Large-Precategory
-    ( unit-Adjunction FG) {X = X} {Y} f =
-    ( inv
-      ( left-unit-law-comp-hom-Large-Precategory C
-        ( comp-hom-Large-Precategory C (η Y) f))) ∙
-      ( ( ap
+    ( unit-Adjunction-Large-Precategory FG) {X = X} {Y} f =
+    inv
+      ( ( inv
+          ( left-unit-law-comp-hom-Large-Precategory C
+            ( comp-hom-Large-Precategory C (η Y) f))) ∙
+        ( ap
           ( comp-hom-Large-Precategory' C
             ( comp-hom-Large-Precategory C (η Y) f))
           ( inv
-            ( preserves-id-right-adjoint-Adjunction C D FG
-              ( obj-left-adjoint-Adjunction C D FG Y)))) ∙
-        ( ( inv
-            ( associative-comp-hom-Large-Precategory C
-              ( hom-right-adjoint-Adjunction C D FG
-                ( id-hom-Large-Precategory D))
-              ( map-inv-equiv-is-adjoint-pair-Adjunction C D FG Y
-                ( obj-left-adjoint-Adjunction C D FG Y)
-                ( id-hom-Large-Precategory D))
-              ( f))) ∙
-          ( ( inv
-              ( naturality-inv-equiv-is-adjoint-pair-Adjunction C D FG f
+            ( preserves-id-right-adjoint-Adjunction-Large-Precategory C D FG
+              ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)))) ∙
+        ( inv
+          ( associative-comp-hom-Large-Precategory C
+            ( hom-right-adjoint-Adjunction-Large-Precategory C D FG
+              ( id-hom-Large-Precategory D))
+            ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory
+              C D FG Y
+              ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)
+              ( id-hom-Large-Precategory D))
+            ( f))) ∙
+        ( inv
+          ( naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory
+            C D FG f
+            ( id-hom-Large-Precategory D)
+            ( id-hom-Large-Precategory D))) ∙
+        ( ap
+          ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG X
+            ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y))
+          ( ( associative-comp-hom-Large-Precategory D
+              ( id-hom-Large-Precategory D)
+              ( id-hom-Large-Precategory D)
+              ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙
+            ( left-unit-law-comp-hom-Large-Precategory D
+              ( comp-hom-Large-Precategory D
                 ( id-hom-Large-Precategory D)
-                ( id-hom-Large-Precategory D))) ∙
-            ( ( ap
-                ( map-inv-equiv-is-adjoint-pair-Adjunction C D FG X
-                  ( obj-left-adjoint-Adjunction C D FG Y))
-                  ( ( associative-comp-hom-Large-Precategory D
-                      ( id-hom-Large-Precategory D)
-                      ( id-hom-Large-Precategory D)
-                      ( hom-left-adjoint-Adjunction C D FG f)) ∙
-                    ( ( left-unit-law-comp-hom-Large-Precategory D
-                        ( comp-hom-Large-Precategory D
-                          ( id-hom-Large-Precategory D)
-                          ( hom-left-adjoint-Adjunction C D FG f))) ∙
-                      ( ( left-unit-law-comp-hom-Large-Precategory D
-                          ( hom-left-adjoint-Adjunction C D FG f)) ∙
-                        ( ( inv
-                            ( right-unit-law-comp-hom-Large-Precategory D
-                              ( hom-left-adjoint-Adjunction C D FG f))) ∙
-                          ( ( inv
-                              ( right-unit-law-comp-hom-Large-Precategory D
-                                ( comp-hom-Large-Precategory D
-                                  ( hom-left-adjoint-Adjunction C D FG f)
-                                  ( id-hom-Large-Precategory D)))) ∙
-                            ( ap
-                              ( comp-hom-Large-Precategory D
-                                ( comp-hom-Large-Precategory D
-                                  ( hom-left-adjoint-Adjunction C D FG f)
-                                  ( id-hom-Large-Precategory D)))
-                              ( inv
-                                ( preserves-id-left-adjoint-Adjunction
-                                  C D FG X))))))))) ∙
-              ( ( naturality-inv-equiv-is-adjoint-pair-Adjunction C D FG
-                  ( id-hom-Large-Precategory C)
-                  ( hom-left-adjoint-Adjunction C D FG f)
-                  ( id-hom-Large-Precategory D)) ∙
-                ( right-unit-law-comp-hom-Large-Precategory C
-                  ( comp-hom-Large-Precategory C
-                    ( hom-right-adjoint-Adjunction C D FG
-                      ( hom-left-adjoint-Adjunction C D FG f))
-                    ( η X))))))))
+                ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
+            ( left-unit-law-comp-hom-Large-Precategory D
+                ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙
+            ( inv
+                ( right-unit-law-comp-hom-Large-Precategory D
+                  ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
+            ( inv
+              ( right-unit-law-comp-hom-Large-Precategory D
+                ( comp-hom-Large-Precategory D
+                  ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)
+                  ( id-hom-Large-Precategory D)))) ∙
+            ( ap
+              ( comp-hom-Large-Precategory D
+                ( comp-hom-Large-Precategory D
+                  ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)
+                  ( id-hom-Large-Precategory D)))
+              ( inv
+                ( preserves-id-left-adjoint-Adjunction-Large-Precategory
+                  C D FG X)))) ∙
+          ( naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory
+            C D FG
+            ( id-hom-Large-Precategory C)
+            ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)
+            ( id-hom-Large-Precategory D)) ∙
+          ( right-unit-law-comp-hom-Large-Precategory C
+            ( comp-hom-Large-Precategory C
+              ( hom-right-adjoint-Adjunction-Large-Precategory C D FG
+                ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))
+              ( η X)))))
     where
     η :
       {l : Level} (X : obj-Large-Precategory C l) →
       type-hom-Large-Precategory C X
-        ( obj-right-adjoint-Adjunction C D FG
-          ( obj-left-adjoint-Adjunction C D FG X))
-    η = obj-natural-transformation-Large-Precategory (unit-Adjunction FG)
+        ( obj-right-adjoint-Adjunction-Large-Precategory C D FG
+          ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X))
+    η =
+      components-natural-transformation-Large-Precategory
+        ( unit-Adjunction-Large-Precategory FG)
 ```
 
 ### Counit of adjunction
@@ -417,79 +503,84 @@ Given an adjoint pair `F ⊣ G`, we can construct a natural transformation
 `ε : F ∘ G → id` called the counit of the adjunction.
 
 ```agda
-  counit-Adjunction :
-    (FG : Adjunction C D) →
+  counit-Adjunction-Large-Precategory :
+    (FG : Adjunction-Large-Precategory C D) →
     natural-transformation-Large-Precategory
       ( comp-functor-Large-Precategory
-        ( left-adjoint-Adjunction FG)
-        ( right-adjoint-Adjunction FG))
+        ( left-adjoint-Adjunction-Large-Precategory FG)
+        ( right-adjoint-Adjunction-Large-Precategory FG))
       ( id-functor-Large-Precategory)
-  obj-natural-transformation-Large-Precategory (counit-Adjunction FG) Y =
-    map-equiv-is-adjoint-pair-Adjunction C D FG
-      ( obj-right-adjoint-Adjunction C D FG Y)
+  components-natural-transformation-Large-Precategory
+    ( counit-Adjunction-Large-Precategory FG) Y =
+    map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG
+      ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y)
       ( Y)
       ( id-hom-Large-Precategory C)
   coherence-square-natural-transformation-Large-Precategory
-    (counit-Adjunction FG) {X = X} {Y = Y} f =
-    ( inv
-      ( left-unit-law-comp-hom-Large-Precategory D
-      ( comp-hom-Large-Precategory D
-        ( ε Y)
-        ( hom-left-adjoint-Adjunction C D FG
-          ( hom-right-adjoint-Adjunction C D FG f))))) ∙
-    ( ( inv
-        ( associative-comp-hom-Large-Precategory D
-          ( id-hom-Large-Precategory D)
-          ( map-equiv-is-adjoint-pair-Adjunction C D FG
-            ( obj-right-adjoint-Adjunction C D FG Y)
-            ( Y)
-            ( id-hom-Large-Precategory C))
-          ( hom-left-adjoint-Adjunction C D FG
-            ( hom-right-adjoint-Adjunction C D FG f)))) ∙
+    (counit-Adjunction-Large-Precategory FG) {X = X} {Y = Y} f =
+    inv
       ( ( inv
-          ( naturality-equiv-is-adjoint-pair-Adjunction C D FG
-            ( hom-right-adjoint-Adjunction C D FG f)
+          ( left-unit-law-comp-hom-Large-Precategory D
+            ( comp-hom-Large-Precategory D
+              ( ε Y)
+              ( hom-left-adjoint-Adjunction-Large-Precategory C D FG
+                ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))))) ∙
+        ( inv
+          ( associative-comp-hom-Large-Precategory D
+            ( id-hom-Large-Precategory D)
+            ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG
+              ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y)
+              ( Y)
+              ( id-hom-Large-Precategory C))
+            ( hom-left-adjoint-Adjunction-Large-Precategory C D FG
+              ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)))) ∙
+        ( inv
+          ( naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG
+            ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)
             ( id-hom-Large-Precategory D)
             ( id-hom-Large-Precategory C))) ∙
-        ( ( ap
-            ( map-equiv-is-adjoint-pair-Adjunction C D FG
-              ( obj-right-adjoint-Adjunction C D FG X)
-              ( Y))
-            ( ( ap
-                ( comp-hom-Large-Precategory' C
-                  ( hom-right-adjoint-Adjunction C D FG f))
-                ( ( right-unit-law-comp-hom-Large-Precategory C
-                    ( hom-right-adjoint-Adjunction C D FG
-                      ( id-hom-Large-Precategory D))) ∙
-                  ( preserves-id-right-adjoint-Adjunction C D FG Y))) ∙
-              ( ( left-unit-law-comp-hom-Large-Precategory C
-                  ( hom-right-adjoint-Adjunction C D FG f)) ∙
-                ( ( inv
-                    ( right-unit-law-comp-hom-Large-Precategory C
-                      ( hom-right-adjoint-Adjunction C D FG f))) ∙
-                  ( inv
-                    ( right-unit-law-comp-hom-Large-Precategory C
-                      ( comp-hom-Large-Precategory C
-                        ( hom-right-adjoint-Adjunction C D FG f)
-                        ( id-hom-Large-Precategory C)))))))) ∙
-          ( ( naturality-equiv-is-adjoint-pair-Adjunction C D FG
-              ( id-hom-Large-Precategory C)
-              ( f)
-              ( id-hom-Large-Precategory C)) ∙
-            ( ( ap
-                ( comp-hom-Large-Precategory
-                  ( D)
-                  ( comp-hom-Large-Precategory D f (ε X)))
-                ( preserves-id-left-adjoint-Adjunction C D FG
-                  ( obj-right-adjoint-Adjunction C D FG X))) ∙
-              ( right-unit-law-comp-hom-Large-Precategory D
-                ( comp-hom-Large-Precategory D f (ε X))))))))
+        ( ap
+          ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG
+            ( obj-right-adjoint-Adjunction-Large-Precategory C D FG X)
+            ( Y))
+          ( ( ap
+              ( comp-hom-Large-Precategory' C
+                ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))
+              ( ( right-unit-law-comp-hom-Large-Precategory C
+                  ( hom-right-adjoint-Adjunction-Large-Precategory C D FG
+                    ( id-hom-Large-Precategory D))) ∙
+                ( preserves-id-right-adjoint-Adjunction-Large-Precategory
+                    C D FG Y))) ∙
+            ( left-unit-law-comp-hom-Large-Precategory C
+              ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)) ∙
+            ( ( inv
+                ( right-unit-law-comp-hom-Large-Precategory C
+                  ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
+              ( inv
+                ( right-unit-law-comp-hom-Large-Precategory C
+                  ( comp-hom-Large-Precategory C
+                    ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)
+                    ( id-hom-Large-Precategory C)))))) ∙
+        ( naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG
+            ( id-hom-Large-Precategory C)
+            ( f)
+            ( id-hom-Large-Precategory C)) ∙
+          ( ap
+            ( comp-hom-Large-Precategory
+              ( D)
+              ( comp-hom-Large-Precategory D f (ε X)))
+            ( preserves-id-left-adjoint-Adjunction-Large-Precategory C D FG
+              ( obj-right-adjoint-Adjunction-Large-Precategory C D FG X))) ∙
+          ( right-unit-law-comp-hom-Large-Precategory D
+            ( comp-hom-Large-Precategory D f (ε X)))))
     where
     ε :
       {l : Level} (Y : obj-Large-Precategory D l) →
       type-hom-Large-Precategory D
-        ( obj-left-adjoint-Adjunction C D FG
-          ( obj-right-adjoint-Adjunction C D FG Y))
+        ( obj-left-adjoint-Adjunction-Large-Precategory C D FG
+          ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y))
         ( Y)
-    ε = obj-natural-transformation-Large-Precategory (counit-Adjunction FG)
+    ε =
+      components-natural-transformation-Large-Precategory
+        ( counit-Adjunction-Large-Precategory FG)
 ```
diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
index 079bd16146..b99bca0d03 100644
--- a/src/category-theory/functors-categories.lagda.md
+++ b/src/category-theory/functors-categories.lagda.md
@@ -52,7 +52,9 @@ module _
     ( F : functor-Category) {x y z : obj-Category C}
     ( g : type-hom-Category C y z) (f : type-hom-Category C x y) →
     ( map-hom-functor-Category F (comp-hom-Category C g f)) ＝
-    ( comp-hom-Category D (map-hom-functor-Category F g) (map-hom-functor-Category F f))
+    ( comp-hom-Category D
+      ( map-hom-functor-Category F g)
+      ( map-hom-functor-Category F f))
   preserves-comp-functor-Category F =
     preserves-comp-functor-Precategory
       ( precategory-Category C)
diff --git a/src/category-theory/functors-large-precategories.lagda.md b/src/category-theory/functors-large-precategories.lagda.md
index 86a52a1738..4d39978810 100644
--- a/src/category-theory/functors-large-precategories.lagda.md
+++ b/src/category-theory/functors-large-precategories.lagda.md
@@ -45,7 +45,8 @@ module _
         obj-Large-Precategory C l1 → obj-Large-Precategory D (γ l1)
       map-hom-functor-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} →
         type-hom-Large-Precategory C X Y →
         type-hom-Large-Precategory D
           ( map-obj-functor-Large-Precategory X)
diff --git a/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md b/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md
index abcd777fc6..8f3780b66a 100644
--- a/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md
+++ b/src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md
@@ -43,8 +43,8 @@ module _
     (α β : natural-transformation-Large-Precategory F G) → UUω
   htpy-natural-transformation-Large-Precategory α β =
     { l : Level} (X : obj-Large-Precategory C l) →
-    ( obj-natural-transformation-Large-Precategory α X) ＝
-    ( obj-natural-transformation-Large-Precategory β X)
+    ( components-natural-transformation-Large-Precategory α X) ＝
+    ( components-natural-transformation-Large-Precategory β X)
 ```
 
 ### The reflexivity homotopy
diff --git a/src/category-theory/natural-isomorphisms-categories.lagda.md b/src/category-theory/natural-isomorphisms-categories.lagda.md
index dc5041b37c..f8c8423c9c 100644
--- a/src/category-theory/natural-isomorphisms-categories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-categories.lagda.md
@@ -32,6 +32,14 @@ module _
   (F G : functor-Category C D)
   where
 
+  iso-family-functor-Category : UU (l1 ⊔ l4)
+  iso-family-functor-Category =
+    iso-family-functor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+
   is-natural-isomorphism-Category :
     natural-transformation-Category C D F G → UU (l1 ⊔ l4)
   is-natural-isomorphism-Category =
diff --git a/src/category-theory/natural-isomorphisms-large-precategories.lagda.md b/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
index 689f3b8518..f24b79c9fa 100644
--- a/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
@@ -19,29 +19,40 @@ open import foundation.universe-levels
 
 ## Idea
 
-A natural isomorphism `γ` from functor `F : C → D` to `G : C → D` is a natural
-transformation from `F` to `G` such that the morphism `γ x : hom (F x) (G x)` is
-an isomorphism, for every object `x` in `C`.
+A **natural isomorphism** `γ` from
+[functor](category-theory.functors-large-precategories.md) `F : C → D` to
+`G : C → D` is a
+[natural transformation](category-theory.natural-transformations-large-precategories.md)
+from `F` to `G` such that the morphism `γ x : hom (F x) (G x)` is an
+[isomorphism](category-theory.isomorphisms-in-precategories.md), for every
+object `x` in `C`.
 
 ## Definition
 
 ```agda
 module _
-  {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level}
-  {C : Large-Precategory αC βC} {D : Large-Precategory αD βD}
+  {αC αD γF γG : Level → Level}
+  {βC βD : Level → Level → Level}
+  {C : Large-Precategory αC βC}
+  {D : Large-Precategory αD βD}
   (F : functor-Large-Precategory C D γF)
   (G : functor-Large-Precategory C D γG)
   where
 
+  iso-family-functor-Large-Precategory : UUω
+  iso-family-functor-Large-Precategory =
+    { l : Level}
+    ( X : obj-Large-Precategory C l) →
+    iso-Large-Precategory D
+      ( map-obj-functor-Large-Precategory F X)
+      ( map-obj-functor-Large-Precategory G X)
+
   record natural-isomorphism-Large-Precategory : UUω
     where
     constructor make-natural-isomorphism
     field
-      obj-natural-isomorphism-Large-Precategory :
-        { l1 : Level} (X : obj-Large-Precategory C l1) →
-        iso-Large-Precategory D
-          ( map-obj-functor-Large-Precategory F X)
-          ( map-obj-functor-Large-Precategory G X)
+      components-natural-isomorphism-Large-Precategory :
+        iso-family-functor-Large-Precategory
       coherence-square-natural-isomorphism-Large-Precategory :
         { l1 l2 : Level}
         { X : obj-Large-Precategory C l1}
@@ -51,25 +62,25 @@ module _
           ( hom-iso-Large-Precategory D
             ( map-obj-functor-Large-Precategory F X)
             ( map-obj-functor-Large-Precategory G X)
-            ( obj-natural-isomorphism-Large-Precategory X))
+            ( components-natural-isomorphism-Large-Precategory X))
           ( map-hom-functor-Large-Precategory F f)
           ( map-hom-functor-Large-Precategory G f)
           ( hom-iso-Large-Precategory D
             ( map-obj-functor-Large-Precategory F Y)
             ( map-obj-functor-Large-Precategory G Y)
-            ( obj-natural-isomorphism-Large-Precategory Y))
+            ( components-natural-isomorphism-Large-Precategory Y))
 
   open natural-isomorphism-Large-Precategory public
 
   natural-transformation-natural-isomorphism-Large-Precategory :
     natural-isomorphism-Large-Precategory →
     natural-transformation-Large-Precategory F G
-  obj-natural-transformation-Large-Precategory
+  components-natural-transformation-Large-Precategory
     ( natural-transformation-natural-isomorphism-Large-Precategory γ) X =
     hom-iso-Large-Precategory D
       ( map-obj-functor-Large-Precategory F X)
       ( map-obj-functor-Large-Precategory G X)
-      ( obj-natural-isomorphism-Large-Precategory γ X)
+      ( components-natural-isomorphism-Large-Precategory γ X)
   coherence-square-natural-transformation-Large-Precategory
     (natural-transformation-natural-isomorphism-Large-Precategory γ) =
       coherence-square-natural-isomorphism-Large-Precategory γ
diff --git a/src/category-theory/natural-isomorphisms-precategories.lagda.md b/src/category-theory/natural-isomorphisms-precategories.lagda.md
index 3c7bb475e4..c29a55c59b 100644
--- a/src/category-theory/natural-isomorphisms-precategories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-precategories.lagda.md
@@ -22,9 +22,13 @@ open import foundation.universe-levels
 
 ## Idea
 
-A natural isomorphism `γ` from functor `F : C → D` to `G : C → D` is a natural
-transformation from `F` to `G` such that the morphism `γ x : hom (F x) (G x)` is
-an isomorphism, for every object `x` in `C`.
+A **natural isomorphism** `γ` from
+[functor](category-theory.functors-precategories.md) `F : C → D` to `G : C → D`
+is a
+[natural transformation](category-theory.natural-transformations-precategories.md)
+from `F` to `G` such that the morphism `γ x : hom (F x) (G x)` is an
+[isomorphism](category-theory.isomorphisms-in-precategories.md), for every
+object `x` in `C`.
 
 ## Definition
 
@@ -36,6 +40,13 @@ module _
   (F G : functor-Precategory C D)
   where
 
+  iso-family-functor-Precategory : UU (l1 ⊔ l4)
+  iso-family-functor-Precategory =
+    (x : obj-Precategory C) →
+    iso-Precategory D
+      ( map-obj-functor-Precategory C D F x)
+      ( map-obj-functor-Precategory C D G x)
+
   is-natural-isomorphism-Precategory :
     natural-transformation-Precategory C D F G → UU (l1 ⊔ l4)
   is-natural-isomorphism-Precategory γ =
diff --git a/src/category-theory/natural-transformations-categories.lagda.md b/src/category-theory/natural-transformations-categories.lagda.md
index e5623c4347..0bde82ea5e 100644
--- a/src/category-theory/natural-transformations-categories.lagda.md
+++ b/src/category-theory/natural-transformations-categories.lagda.md
@@ -39,12 +39,16 @@ module _
   (F G : functor-Category C D)
   where
 
+  hom-family-functor-Category : UU (l1 ⊔ l4)
+  hom-family-functor-Category =
+    hom-family-functor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+
   is-natural-transformation-Category :
-    ( ( x : obj-Category C) →
-      type-hom-Category D
-        ( map-obj-functor-Category C D F x)
-        ( map-obj-functor-Category C D G x)) →
-    UU (l1 ⊔ l2 ⊔ l4)
+    hom-family-functor-Category → UU (l1 ⊔ l2 ⊔ l4)
   is-natural-transformation-Category =
     is-natural-transformation-Precategory
       ( precategory-Category C)
@@ -61,10 +65,7 @@ module _
       ( G)
 
   components-natural-transformation-Category :
-    natural-transformation-Category → (x : obj-Category C) →
-    type-hom-Category D
-      ( map-obj-functor-Category C D F x)
-      ( map-obj-functor-Category C D G x)
+    natural-transformation-Category → hom-family-functor-Category
   components-natural-transformation-Category =
     components-natural-transformation-Precategory
       ( precategory-Category C)
@@ -125,11 +126,7 @@ module _
   where
 
   is-prop-is-natural-transformation-Category :
-    ( γ :
-      (x : obj-Category C) →
-      type-hom-Category D
-        ( map-obj-functor-Category C D F x)
-        ( map-obj-functor-Category C D G x)) →
+    ( γ : hom-family-functor-Category C D F G) →
     is-prop (is-natural-transformation-Category C D F G γ)
   is-prop-is-natural-transformation-Category =
     is-prop-is-natural-transformation-Precategory
@@ -139,12 +136,7 @@ module _
       ( G)
 
   is-natural-transformation-Category-Prop :
-    ( γ :
-      (x : obj-Category C) →
-      type-hom-Category D
-        ( map-obj-functor-Category C D F x)
-        ( map-obj-functor-Category C D G x)) →
-    Prop (l1 ⊔ l2 ⊔ l4)
+    ( γ : hom-family-functor-Category C D F G) → Prop (l1 ⊔ l2 ⊔ l4)
   is-natural-transformation-Category-Prop =
     is-natural-transformation-Precategory-Prop
       ( precategory-Category C)
@@ -165,8 +157,7 @@ module _
       ( F)
       ( G)
 
-  natural-transformation-Category-Set :
-    Set (l1 ⊔ l2 ⊔ l4)
+  natural-transformation-Category-Set : Set (l1 ⊔ l2 ⊔ l4)
   natural-transformation-Category-Set =
     natural-transformation-Precategory-Set
       ( precategory-Category C)
diff --git a/src/category-theory/natural-transformations-large-precategories.lagda.md b/src/category-theory/natural-transformations-large-precategories.lagda.md
index 09776c4343..88f1efca80 100644
--- a/src/category-theory/natural-transformations-large-precategories.lagda.md
+++ b/src/category-theory/natural-transformations-large-precategories.lagda.md
@@ -44,8 +44,8 @@ square-Large-Precategory :
   (bottom : type-hom-Large-Precategory C X Y) →
   UU (βC l1 l4)
 square-Large-Precategory C top left right bottom =
-  comp-hom-Large-Precategory C bottom left ＝
-  comp-hom-Large-Precategory C right top
+  comp-hom-Large-Precategory C right top ＝
+  comp-hom-Large-Precategory C bottom left
 
 module _
   {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level}
@@ -53,15 +53,19 @@ module _
   (F : functor-Large-Precategory C D γF) (G : functor-Large-Precategory C D γG)
   where
 
+  hom-family-functor-Large-Precategory : UUω
+  hom-family-functor-Large-Precategory =
+    {l : Level} (X : obj-Large-Precategory C l) →
+    type-hom-Large-Precategory D
+      ( map-obj-functor-Large-Precategory F X)
+      ( map-obj-functor-Large-Precategory G X)
+
   record natural-transformation-Large-Precategory : UUω
     where
     constructor make-natural-transformation
     field
       components-natural-transformation-Large-Precategory :
-        {l1 : Level} (X : obj-Large-Precategory C l1) →
-        type-hom-Large-Precategory D
-          ( map-obj-functor-Large-Precategory F X)
-          ( map-obj-functor-Large-Precategory G X)
+        hom-family-functor-Large-Precategory
       coherence-square-natural-transformation-Large-Precategory :
         {l1 l2 : Level} {X : obj-Large-Precategory C l1}
         {Y : obj-Large-Precategory C l2}
@@ -97,9 +101,57 @@ module _
       id-hom-Large-Precategory D
   coherence-square-natural-transformation-Large-Precategory
     ( id-natural-transformation-Large-Precategory F) f =
-    ( left-unit-law-comp-hom-Large-Precategory D
-      ( map-hom-functor-Large-Precategory F f)) ∙
+        ( right-unit-law-comp-hom-Large-Precategory D
+          ( map-hom-functor-Large-Precategory F f)) ∙
+        ( inv
+          ( left-unit-law-comp-hom-Large-Precategory D
+            ( map-hom-functor-Large-Precategory F f)))
+```
+
+### Composition of natural transformations
+
+```agda
+module _
+  { αC αD γF γG γH : Level → Level}
+  { βC βD : Level → Level → Level}
+  { C : Large-Precategory αC βC}
+  { D : Large-Precategory αD βD}
+  where
+
+  comp-natural-transformation-Large-Precategory :
+    (F : functor-Large-Precategory C D γF) →
+    (G : functor-Large-Precategory C D γG) →
+    (H : functor-Large-Precategory C D γH) →
+    natural-transformation-Large-Precategory G H →
+    natural-transformation-Large-Precategory F G →
+    natural-transformation-Large-Precategory F H
+  components-natural-transformation-Large-Precategory
+    ( comp-natural-transformation-Large-Precategory F G H b a) X =
+      comp-hom-Large-Precategory D
+        ( components-natural-transformation-Large-Precategory b X)
+        ( components-natural-transformation-Large-Precategory a X)
+  coherence-square-natural-transformation-Large-Precategory
+    ( comp-natural-transformation-Large-Precategory F G H b a) {X = X} {Y} f =
+    ( inv
+      ( associative-comp-hom-Large-Precategory D
+        ( map-hom-functor-Large-Precategory H f)
+        ( components-natural-transformation-Large-Precategory b X)
+        ( components-natural-transformation-Large-Precategory a X))) ∙
+    ( ap
+      ( comp-hom-Large-Precategory' D
+        ( components-natural-transformation-Large-Precategory a X))
+      ( coherence-square-natural-transformation-Large-Precategory b f)) ∙
+    ( associative-comp-hom-Large-Precategory D
+      ( components-natural-transformation-Large-Precategory b Y)
+      ( map-hom-functor-Large-Precategory G f)
+      ( components-natural-transformation-Large-Precategory a X)) ∙
+    ( ap
+      ( comp-hom-Large-Precategory D
+        ( components-natural-transformation-Large-Precategory b Y))
+      ( coherence-square-natural-transformation-Large-Precategory a f)) ∙
     ( inv
-      ( right-unit-law-comp-hom-Large-Precategory D
+      ( associative-comp-hom-Large-Precategory D
+        ( components-natural-transformation-Large-Precategory b Y)
+        ( components-natural-transformation-Large-Precategory a Y)
         ( map-hom-functor-Large-Precategory F f)))
 ```
diff --git a/src/category-theory/natural-transformations-precategories.lagda.md b/src/category-theory/natural-transformations-precategories.lagda.md
index 6fcdb90c6a..b9a9a9ca03 100644
--- a/src/category-theory/natural-transformations-precategories.lagda.md
+++ b/src/category-theory/natural-transformations-precategories.lagda.md
@@ -46,12 +46,15 @@ module _
   (F G : functor-Precategory C D)
   where
 
+  hom-family-functor-Precategory : UU (l1 ⊔ l4)
+  hom-family-functor-Precategory =
+    (x : obj-Precategory C) →
+    type-hom-Precategory D
+      ( map-obj-functor-Precategory C D F x)
+      ( map-obj-functor-Precategory C D G x)
+
   is-natural-transformation-Precategory :
-    ( (x : obj-Precategory C) →
-      type-hom-Precategory D
-        ( map-obj-functor-Precategory C D F x)
-        ( map-obj-functor-Precategory C D G x)) →
-    UU (l1 ⊔ l2 ⊔ l4)
+    hom-family-functor-Precategory → UU (l1 ⊔ l2 ⊔ l4)
   is-natural-transformation-Precategory γ =
     {x y : obj-Precategory C} (f : type-hom-Precategory C x y) →
     ( comp-hom-Precategory D (map-hom-functor-Precategory C D G f) (γ x)) ＝
@@ -59,18 +62,12 @@ module _
 
   natural-transformation-Precategory : UU (l1 ⊔ l2 ⊔ l4)
   natural-transformation-Precategory =
-    Σ ( (x : obj-Precategory C) →
-        type-hom-Precategory D
-          ( map-obj-functor-Precategory C D F x)
-          ( map-obj-functor-Precategory C D G x))
-      is-natural-transformation-Precategory
+    Σ ( hom-family-functor-Precategory)
+      ( is-natural-transformation-Precategory)
 
   components-natural-transformation-Precategory :
     natural-transformation-Precategory →
-    (x : obj-Precategory C) →
-    type-hom-Precategory D
-      ( map-obj-functor-Precategory C D F x)
-      ( map-obj-functor-Precategory C D G x)
+    hom-family-functor-Precategory
   components-natural-transformation-Precategory = pr1
 
   coherence-square-natural-transformation-Precategory :
@@ -149,11 +146,7 @@ module _
   where
 
   is-prop-is-natural-transformation-Precategory :
-    ( γ :
-      (x : obj-Precategory C) →
-      type-hom-Precategory D
-        ( map-obj-functor-Precategory C D F x)
-        ( map-obj-functor-Precategory C D G x)) →
+    ( γ : hom-family-functor-Precategory C D F G) →
     is-prop (is-natural-transformation-Precategory C D F G γ)
   is-prop-is-natural-transformation-Precategory γ =
     is-prop-Π'
@@ -173,12 +166,7 @@ module _
                     ( map-hom-functor-Precategory C D F f)))))
 
   is-natural-transformation-Precategory-Prop :
-    ( γ :
-      (x : obj-Precategory C) →
-      type-hom-Precategory D
-        ( map-obj-functor-Precategory C D F x)
-        ( map-obj-functor-Precategory C D G x)) →
-    Prop (l1 ⊔ l2 ⊔ l4)
+    ( γ : hom-family-functor-Precategory C D F G) → Prop (l1 ⊔ l2 ⊔ l4)
   pr1 (is-natural-transformation-Precategory-Prop α) =
     is-natural-transformation-Precategory C D F G α
   pr2 (is-natural-transformation-Precategory-Prop α) =