small fixes

fredrik-bakke · Sep 18, 2023 · 43ee8e8 · 43ee8e8
1 parent 51ec628
commit 43ee8e8
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git a/src/category-theory/natural-transformations-precategories.lagda.md b/src/category-theory/natural-transformations-precategories.lagda.md
@@ -66,7 +66,8 @@ module _
       is-natural-transformation-Precategory
 
   components-natural-transformation-Precategory :
-    natural-transformation-Precategory → (x : obj-Precategory C) →
+    natural-transformation-Precategory →
+    (x : obj-Precategory C) →
     type-hom-Precategory D
       ( obj-functor-Precategory C D F x)
       ( obj-functor-Precategory C D G x)
@@ -92,8 +93,9 @@ 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 _ ∙
-    inv (left-unit-law-comp-hom-Precategory D _)
+    ( right-unit-law-comp-hom-Precategory D (hom-functor-Precategory C D F f)) ∙
+    ( inv
+      ( left-unit-law-comp-hom-Precategory D (hom-functor-Precategory C D F f)))
 
   comp-natural-transformation-Precategory :
     (F G H : functor-Precategory C D) →

diff --git a/src/category-theory/precategory-of-functors.lagda.md b/src/category-theory/precategory-of-functors.lagda.md
@@ -23,7 +23,8 @@ open import foundation.universe-levels
 [precategories](category-theory.precategories.md) and
 [natural transformations](category-theory.natural-transformations-precategories.md)
 between them introduce a new precategory whose identity map and composition
-structure are inherited pointwise from the codomain precategory.
+structure are inherited pointwise from the codomain precategory. This is called
+the **precategory of functors**.
 
 ## Definition
 
@@ -35,8 +36,8 @@ module _
   functor-precategory-Precategory :
     Precategory (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l2 ⊔ l4)
   pr1 functor-precategory-Precategory = functor-Precategory C D
-  pr1 (pr2 functor-precategory-Precategory) F G =
-    natural-transformation-Precategory-Set C D F G
+  pr1 (pr2 functor-precategory-Precategory) =
+    natural-transformation-Precategory-Set C D
   pr1 (pr2 (pr2 functor-precategory-Precategory)) =
     ( λ {F} {G} {H} → comp-natural-transformation-Precategory C D F G H) ,
     ( λ {F} {G} {H} {I} h g f →

diff --git a/src/category-theory/representing-arrow-category.lagda.md b/src/category-theory/representing-arrow-category.lagda.md
@@ -164,4 +164,5 @@ pr2 representing-arrow-Category = is-category-representing-arrow
 
 ### The representing arrow represents arrows in a category
 
-Use the Yoneda lemma.
+This is a consequence of the
+[Yoneda lemma](category-theory.yoneda-lemma-categories).