comp-natural-transformation-Large-Precategory and associated refact…

…oring
fredrik-bakke · Sep 19, 2023 · 65483f6 · 65483f6
1 parent 9c166ae
commit 65483f6
Show file tree

Hide file tree

Showing 10 changed files with 484 additions and 329 deletions.
diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
diff --git 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
@@ -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/...category-theory/homotopies-natural-transformations-large-precategories.lagda.md b/...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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -44,24 +44,28 @@ 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}
   {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
 
+  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
@@ -46,31 +46,28 @@ 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)) ＝
     ( comp-hom-Precategory D (γ y) (map-hom-functor-Precategory C D F f))
 
   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 α) =