pre-commit

fredrik-bakke · Sep 18, 2023 · 9c166ae · 9c166ae
1 parent 08af608
commit 9c166ae
Show file tree

Hide file tree

Showing 8 changed files with 64 additions and 39 deletions.
diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
@@ -59,8 +59,12 @@ module _
       equiv-is-adjoint-pair-Large-Precategory :
         {l1 l2 : Level} (X : obj-Large-Precategory C l1)
         (Y : obj-Large-Precategory D l2) →
-        ( type-hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y)) ≃
-        ( 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)) ≃
+        ( type-hom-Large-Precategory D
+          ( map-obj-functor-Large-Precategory F X)
+          ( 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}
@@ -121,7 +125,9 @@ module _
           ( map-hom-functor-Large-Precategory F f))
       ( λ h →
         comp-hom-Large-Precategory C
-          ( comp-hom-Large-Precategory C (map-hom-functor-Large-Precategory G g) h)
+          ( comp-hom-Large-Precategory C
+            ( map-hom-functor-Large-Precategory G g)
+            ( h))
           ( f))
       ( map-inv-equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
   naturality-inv-equiv-is-adjoint-pair-Large-Precategory
@@ -130,7 +136,9 @@ module _
       ( equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
       ( λ h →
         comp-hom-Large-Precategory C
-          ( comp-hom-Large-Precategory C (map-hom-functor-Large-Precategory G g) h)
+          ( comp-hom-Large-Precategory C
+            ( map-hom-functor-Large-Precategory G g)
+            ( h))
           ( f))
       ( λ h →
         comp-hom-Large-Precategory D

diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
@@ -43,7 +43,9 @@ module _
     (F : functor-Category) →
     {x y : obj-Category C} →
     (f : type-hom-Category C x y) →
-    type-hom-Category D (map-obj-functor-Category F x) (map-obj-functor-Category F y)
+    type-hom-Category D
+      ( map-obj-functor-Category F x)
+      ( map-obj-functor-Category F y)
   map-hom-functor-Category F = pr1 (pr2 F)
 
   preserves-comp-functor-Category :

diff --git a/src/category-theory/functors-large-precategories.lagda.md b/src/category-theory/functors-large-precategories.lagda.md
@@ -57,13 +57,15 @@ module _
         { Z : obj-Large-Precategory C l3}
         ( g : type-hom-Large-Precategory C Y Z)
         ( f : type-hom-Large-Precategory C X Y) →
-        ( map-hom-functor-Large-Precategory (comp-hom-Large-Precategory C g f)) ＝
+        ( map-hom-functor-Large-Precategory
+          ( comp-hom-Large-Precategory C g f)) ＝
         ( comp-hom-Large-Precategory D
           ( map-hom-functor-Large-Precategory g)
           ( map-hom-functor-Large-Precategory f))
       preserves-id-functor-Large-Precategory :
         { l1 : Level} {X : obj-Large-Precategory C l1} →
-        ( map-hom-functor-Large-Precategory (id-hom-Large-Precategory C {X = X})) ＝
+        ( map-hom-functor-Large-Precategory
+          ( id-hom-Large-Precategory C {X = X})) ＝
         ( id-hom-Large-Precategory D {X = map-obj-functor-Large-Precategory X})
 
   open functor-Large-Precategory public

diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md
@@ -122,7 +122,8 @@ pr2 (pr2 (pr2 (comp-functor-Precategory C D E G F))) x =
   ( ap
     ( map-hom-functor-Precategory D E G)
     ( preserves-id-functor-Precategory C D F x)) ∙
-  ( preserves-id-functor-Precategory D E G (map-obj-functor-Precategory C D F x))
+  ( preserves-id-functor-Precategory D E G
+    ( map-obj-functor-Precategory C D F x))
 ```
 
 ## Properties

diff --git a/src/category-theory/natural-transformations-large-precategories.lagda.md b/src/category-theory/natural-transformations-large-precategories.lagda.md
@@ -10,6 +10,8 @@ module category-theory.natural-transformations-large-precategories where
 open import category-theory.functors-large-precategories
 open import category-theory.large-precategories
 
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
 ```
@@ -18,8 +20,10 @@ open import foundation.universe-levels
 
 ## Idea
 
-Given large precategories `C` and `D`, a natural transformation from a functor
-`F : C → D` to `G : C → D` consists of :
+Given [large precategories](category-theory.large-precategories.md) `C` and `D`,
+a **natural transformation** from a
+[functor](category-theory.functors-large-precategories.md) `F : C → D` to
+`G : C → D` consists of :
 
 - a family of morphisms `γ : (x : C) → hom (F x) (G x)` such that the following
   identity holds:
@@ -53,45 +57,49 @@ module _
     where
     constructor make-natural-transformation
     field
-      obj-natural-transformation-Large-Precategory :
+      components-natural-transformation-Large-Precategory :
         {l1 : Level} (X : obj-Large-Precategory C l1) →
         type-hom-Large-Precategory D
-          ( obj-functor-Large-Precategory F X)
-          ( obj-functor-Large-Precategory G X)
+          ( map-obj-functor-Large-Precategory F X)
+          ( map-obj-functor-Large-Precategory G X)
       coherence-square-natural-transformation-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) →
         square-Large-Precategory D
-          ( obj-natural-transformation-Large-Precategory X)
-          ( hom-functor-Large-Precategory F f)
-          ( hom-functor-Large-Precategory G f)
-          ( obj-natural-transformation-Large-Precategory Y)
+          ( components-natural-transformation-Large-Precategory X)
+          ( map-hom-functor-Large-Precategory F f)
+          ( map-hom-functor-Large-Precategory G f)
+          ( components-natural-transformation-Large-Precategory Y)
 
   open natural-transformation-Large-Precategory public
 ```
 
-## Examples
+## Properties
 
 ### The identity natural transformation
 
 Every functor comes equipped with an identity natural transformation.
 
 ```agda
-id-natural-transformation-Large-Precategory :
-  { α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) →
-  natural-transformation-Large-Precategory F F
-obj-natural-transformation-Large-Precategory
-  ( id-natural-transformation-Large-Precategory {D = D} F) X =
-    id-hom-Large-Precategory D
-coherence-square-natural-transformation-Large-Precategory
-  ( id-natural-transformation-Large-Precategory {D = D} F) f =
-  ( left-unit-law-comp-hom-Large-Precategory D
-    ( hom-functor-Large-Precategory F f)) ∙
-  ( inv
-    ( right-unit-law-comp-hom-Large-Precategory D
-      ( hom-functor-Large-Precategory F f)))
+module _
+  { αC αD γF : Level → Level}
+  { βC βD : Level → Level → Level}
+  { C : Large-Precategory αC βC}
+  { D : Large-Precategory αD βD}
+  where
+
+  id-natural-transformation-Large-Precategory :
+    ( F : functor-Large-Precategory C D γF) →
+    natural-transformation-Large-Precategory F F
+  components-natural-transformation-Large-Precategory
+    ( id-natural-transformation-Large-Precategory F) X =
+      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)) ∙
+    ( inv
+      ( right-unit-law-comp-hom-Large-Precategory D
+        ( 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
@@ -93,9 +93,11 @@ module _
     (F : functor-Precategory C D) → natural-transformation-Precategory C D F F
   pr1 (id-natural-transformation-Precategory F) x = id-hom-Precategory D
   pr2 (id-natural-transformation-Precategory F) f =
-    ( right-unit-law-comp-hom-Precategory D (map-hom-functor-Precategory C D F f)) ∙
+    ( right-unit-law-comp-hom-Precategory D
+      ( map-hom-functor-Precategory C D F f)) ∙
     ( inv
-      ( left-unit-law-comp-hom-Precategory D (map-hom-functor-Precategory C D F f)))
+      ( left-unit-law-comp-hom-Precategory D
+        ( map-hom-functor-Precategory C D F f)))
 
   comp-natural-transformation-Precategory :
     (F G H : functor-Precategory C D) →
@@ -200,7 +202,9 @@ module _
           is-set-type-hom-Precategory D
             ( map-obj-functor-Precategory C D F x)
             ( map-obj-functor-Precategory C D G x)))
-      ( λ α → is-set-type-Set (set-Prop (is-natural-transformation-Precategory-Prop α)))
+      ( λ α →
+        is-set-type-Set
+          ( set-Prop (is-natural-transformation-Precategory-Prop α)))
 
   natural-transformation-Precategory-Set :
     Set (l1 ⊔ l2 ⊔ l4)

diff --git a/src/foundation/booleans.lagda.md b/src/foundation/booleans.lagda.md
@@ -66,7 +66,7 @@ compute-raise-bool : (l : Level) → bool ≃ raise-bool l
 compute-raise-bool l = compute-raise l bool
 ```
 
-### The representing propositions of bool
+### The standard propositions associated to the constructors of bool
 
 ```agda
 prop-bool : bool → Prop lzero

diff --git a/src/group-theory/substitution-functor-group-actions.lagda.md b/src/group-theory/substitution-functor-group-actions.lagda.md
@@ -91,7 +91,7 @@ module _
       ( λ l → l)
   map-obj-functor-Large-Precategory subst-Abstract-Group-Action =
     obj-subst-Abstract-Group-Action
-  map-hom-functor-Large-Precategory subst-Abstract-Group-Action {l1} {l2} {X} {Y} =
+  map-hom-functor-Large-Precategory subst-Abstract-Group-Action {X = X} {Y} =
     hom-subst-Abstract-Group-Action X Y
   preserves-comp-functor-Large-Precategory subst-Abstract-Group-Action
     {l1} {l2} {l3} {X} {Y} {Z} =