reversing naturality (#856)

UniMath · Oct 17, 2023 · 8ebe42b · 8ebe42b
1 parent 786f98a
commit 8ebe42b
Show file tree

Hide file tree

Showing 4 changed files with 154 additions and 150 deletions.
diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
@@ -427,77 +427,79 @@ module _
         ( left-adjoint-Adjunction-Large-Precategory FG))
       ( hom-unit-Adjunction-Large-Precategory)
   naturality-unit-Adjunction-Large-Precategory {X = X} {Y} f =
-    ( inv
-      ( left-unit-law-comp-hom-Large-Precategory C
-        ( comp-hom-Large-Precategory C
-          ( hom-unit-Adjunction-Large-Precategory
-            ( Y))
-          ( f)))) ∙
-    ( ap
-      ( comp-hom-Large-Precategory' C
-        ( comp-hom-Large-Precategory C
-          ( hom-unit-Adjunction-Large-Precategory
-            ( Y))
-          ( f)))
-      ( inv
-        ( 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)
-            ( 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
+      ( ( inv
+          ( left-unit-law-comp-hom-Large-Precategory C
+            ( comp-hom-Large-Precategory C
+              ( hom-unit-Adjunction-Large-Precategory
+                ( Y))
+              ( f)))) ∙
+        ( ap
+          ( comp-hom-Large-Precategory' C
+            ( comp-hom-Large-Precategory C
+              ( hom-unit-Adjunction-Large-Precategory
+                ( Y))
+              ( f)))
+          ( inv
+            ( preserves-id-right-adjoint-Adjunction-Large-Precategory
+              ( C)
+              ( D)
+              ( FG)
+              ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)))) ∙
         ( inv
-          ( right-unit-law-comp-hom-Large-Precategory D
-            ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
+          ( 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
-          ( 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)))) ∙
+          ( naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory
+            C D FG f
+            ( id-hom-Large-Precategory D)
+            ( 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))
-          ( hom-unit-Adjunction-Large-Precategory
-            ( X)))))
+          ( 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)
+                ( 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))
+              ( hom-unit-Adjunction-Large-Precategory
+                ( X))))))
 
   unit-Adjunction-Large-Precategory :
     natural-transformation-Large-Precategory C C
@@ -545,68 +547,69 @@ module _
       ( id-functor-Large-Precategory D)
       ( hom-counit-Adjunction-Large-Precategory)
   naturality-counit-Adjunction-Large-Precategory {X = X} {Y = Y} f =
-    ( inv
-      ( left-unit-law-comp-hom-Large-Precategory D
-        ( comp-hom-Large-Precategory D
-          ( hom-counit-Adjunction-Large-Precategory
+    inv
+      ( ( inv
+          ( left-unit-law-comp-hom-Large-Precategory D
+            ( comp-hom-Large-Precategory D
+              ( hom-counit-Adjunction-Large-Precategory
+                ( 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-Large-Precategory C D FG
+            ( obj-right-adjoint-Adjunction-Large-Precategory C D FG X)
             ( 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-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
-            ( hom-counit-Adjunction-Large-Precategory
-              ( 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
-          ( hom-counit-Adjunction-Large-Precategory
-            ( X)))))
+          ( ( 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
+                ( hom-counit-Adjunction-Large-Precategory
+                  ( 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
+              ( hom-counit-Adjunction-Large-Precategory
+                ( X))))))
 
   counit-Adjunction-Large-Precategory :
     natural-transformation-Large-Precategory D D

diff --git a/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md b/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md
@@ -60,12 +60,12 @@ module _
         { Y : obj-Large-Precategory C l2}
         ( f : hom-Large-Precategory C X Y) →
         coherence-square-hom-Large-Precategory D
+          ( hom-functor-Large-Precategory F f)
           ( hom-iso-Large-Precategory D
             ( iso-natural-isomorphism-Large-Precategory X))
-          ( hom-functor-Large-Precategory F f)
-          ( hom-functor-Large-Precategory G f)
           ( hom-iso-Large-Precategory D
             ( iso-natural-isomorphism-Large-Precategory Y))
+          ( hom-functor-Large-Precategory G f)
 
   open natural-isomorphism-Large-Precategory public
 

diff --git a/src/category-theory/natural-transformations-functors-large-precategories.lagda.md b/src/category-theory/natural-transformations-functors-large-precategories.lagda.md
@@ -55,10 +55,10 @@ module _
     {Y : obj-Large-Precategory C l2}
     (f : hom-Large-Precategory C X Y) →
     coherence-square-hom-Large-Precategory D
-      ( τ X)
       ( hom-functor-Large-Precategory F f)
-      ( hom-functor-Large-Precategory G f)
+      ( τ X)
       ( τ Y)
+      ( hom-functor-Large-Precategory G f)
 
   record natural-transformation-Large-Precategory : UUω
     where
@@ -97,10 +97,10 @@ module _
     naturality-family-of-morphisms-functor-Large-Precategory C D F F
       hom-id-natural-transformation-Large-Precategory
   naturality-id-natural-transformation-Large-Precategory f =
-    ( left-unit-law-comp-hom-Large-Precategory D
-      ( hom-functor-Large-Precategory F f)) ∙
+    ( right-unit-law-comp-hom-Large-Precategory D
+        ( hom-functor-Large-Precategory F f)) ∙
     ( inv
-      ( right-unit-law-comp-hom-Large-Precategory D
+      ( left-unit-law-comp-hom-Large-Precategory D
         ( hom-functor-Large-Precategory F f)))
 
   id-natural-transformation-Large-Precategory :
@@ -139,27 +139,28 @@ module _
     naturality-family-of-morphisms-functor-Large-Precategory C D F H
       hom-comp-natural-transformation-Large-Precategory
   naturality-comp-natural-transformation-Large-Precategory {X = X} {Y} f =
+    inv
+      ( associative-comp-hom-Large-Precategory D
+        ( hom-functor-Large-Precategory H f)
+        ( hom-natural-transformation-Large-Precategory τ X)
+        ( hom-natural-transformation-Large-Precategory σ X)) ∙
+    ( ap
+      ( comp-hom-Large-Precategory' D
+        ( hom-natural-transformation-Large-Precategory σ X))
+      ( naturality-natural-transformation-Large-Precategory τ f)) ∙
     ( associative-comp-hom-Large-Precategory D
       ( hom-natural-transformation-Large-Precategory τ Y)
-      ( hom-natural-transformation-Large-Precategory σ Y)
-      ( hom-functor-Large-Precategory F f)) ∙
+      ( hom-functor-Large-Precategory G f)
+      ( hom-natural-transformation-Large-Precategory σ X)) ∙
     ( ap
       ( comp-hom-Large-Precategory D
         ( hom-natural-transformation-Large-Precategory τ Y))
       ( naturality-natural-transformation-Large-Precategory σ f)) ∙
     ( inv
-      ( associative-comp-hom-Large-Precategory D
+      (associative-comp-hom-Large-Precategory D
         ( hom-natural-transformation-Large-Precategory τ Y)
-        ( hom-functor-Large-Precategory G f)
-        ( hom-natural-transformation-Large-Precategory σ X))) ∙
-    ( ap
-      ( comp-hom-Large-Precategory' D
-        ( hom-natural-transformation-Large-Precategory σ X))
-      ( naturality-natural-transformation-Large-Precategory τ f)) ∙
-    ( associative-comp-hom-Large-Precategory D
-      ( hom-functor-Large-Precategory H f)
-      ( hom-natural-transformation-Large-Precategory τ X)
-      ( hom-natural-transformation-Large-Precategory σ X))
+        ( hom-natural-transformation-Large-Precategory σ Y)
+        ( hom-functor-Large-Precategory F f)))
 
   comp-natural-transformation-Large-Precategory :
     natural-transformation-Large-Precategory C D F H

diff --git a/src/category-theory/representable-functors-large-precategories.lagda.md b/src/category-theory/representable-functors-large-precategories.lagda.md
@@ -126,7 +126,7 @@ module _
       ( representable-functor-Large-Precategory C b)
       ( hom-representable-natural-transformation-Large-Precategory)
   naturality-representable-natural-transformation-Large-Precategory h =
-    eq-htpy (λ g → associative-comp-hom-Large-Precategory C h g f)
+    inv (eq-htpy (λ g → associative-comp-hom-Large-Precategory C h g f))
 
   representable-natural-transformation-Large-Precategory :
     natural-transformation-Large-Precategory C Set-Large-Precategory