fix hom-set function categories

fredrik-bakke · Sep 21, 2023 · 3a646ce · 3a646ce
1 parent 3bfc7dd
commit 3a646ce
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 18 deletions.
diff --git a/src/category-theory/dependent-products-of-categories.lagda.md b/src/category-theory/dependent-products-of-categories.lagda.md
@@ -59,9 +59,9 @@ module _
   obj-Π-Category : UU (l1 ⊔ l2)
   obj-Π-Category = obj-Category Π-Category
 
-  hom-Π-Category :
+  hom-set-Π-Category :
     obj-Π-Category → obj-Π-Category → Set (l1 ⊔ l3)
-  hom-Π-Category = hom-set-Category Π-Category
+  hom-set-Π-Category = hom-set-Category Π-Category
 
   hom-Π-Category :
     obj-Π-Category → obj-Π-Category → UU (l1 ⊔ l3)
@@ -85,7 +85,7 @@ module _
     associative-comp-hom-Category Π-Category
 
   associative-composition-structure-Π-Category :
-    associative-composition-structure-Set hom-Π-Category
+    associative-composition-structure-Set hom-set-Π-Category
   associative-composition-structure-Π-Category =
     associative-composition-structure-Category Π-Category
 
@@ -108,7 +108,7 @@ module _
 
   is-unital-Π-Category :
     is-unital-composition-structure-Set
-      hom-Π-Category
+      hom-set-Π-Category
       associative-composition-structure-Π-Category
   is-unital-Π-Category = is-unital-composition-structure-Category Π-Category
 

diff --git a/src/category-theory/dependent-products-of-precategories.lagda.md b/src/category-theory/dependent-products-of-precategories.lagda.md
@@ -39,11 +39,12 @@ module _
   obj-Π-Precategory : UU (l1 ⊔ l2)
   obj-Π-Precategory = (i : I) → obj-Precategory (C i)
 
-  hom-Π-Precategory : obj-Π-Precategory → obj-Π-Precategory → Set (l1 ⊔ l3)
-  hom-Π-Precategory x y = Π-Set' I (λ i → hom-set-Precategory (C i) (x i) (y i))
+  hom-set-Π-Precategory : obj-Π-Precategory → obj-Π-Precategory → Set (l1 ⊔ l3)
+  hom-set-Π-Precategory x y =
+    Π-Set' I (λ i → hom-set-Precategory (C i) (x i) (y i))
 
   hom-Π-Precategory : obj-Π-Precategory → obj-Π-Precategory → UU (l1 ⊔ l3)
-  hom-Π-Precategory x y = type-Set (hom-Π-Precategory x y)
+  hom-Π-Precategory x y = type-Set (hom-set-Π-Precategory x y)
 
   comp-hom-Π-Precategory :
     {x y z : obj-Π-Precategory} →
@@ -63,7 +64,7 @@ module _
     eq-htpy (λ i → associative-comp-hom-Precategory (C i) (h i) (g i) (f i))
 
   associative-composition-structure-Π-Precategory :
-    associative-composition-structure-Set hom-Π-Precategory
+    associative-composition-structure-Set hom-set-Π-Precategory
   pr1 associative-composition-structure-Π-Precategory = comp-hom-Π-Precategory
   pr2 associative-composition-structure-Π-Precategory =
     associative-comp-hom-Π-Precategory
@@ -86,15 +87,15 @@ module _
 
   is-unital-Π-Precategory :
     is-unital-composition-structure-Set
-      hom-Π-Precategory
+      hom-set-Π-Precategory
       associative-composition-structure-Π-Precategory
   pr1 is-unital-Π-Precategory x = id-hom-Π-Precategory
   pr1 (pr2 is-unital-Π-Precategory) = left-unit-law-comp-hom-Π-Precategory
   pr2 (pr2 is-unital-Π-Precategory) = right-unit-law-comp-hom-Π-Precategory
 
   Π-Precategory : Precategory (l1 ⊔ l2) (l1 ⊔ l3)
   pr1 Π-Precategory = obj-Π-Precategory
-  pr1 (pr2 Π-Precategory) = hom-Π-Precategory
+  pr1 (pr2 Π-Precategory) = hom-set-Π-Precategory
   pr1 (pr2 (pr2 Π-Precategory)) =
     associative-composition-structure-Π-Precategory
   pr2 (pr2 (pr2 Π-Precategory)) = is-unital-Π-Precategory

diff --git a/src/category-theory/function-categories.lagda.md b/src/category-theory/function-categories.lagda.md
@@ -47,9 +47,9 @@ module _
   obj-function-Category : UU (l1 ⊔ l2)
   obj-function-Category = obj-Category function-Category
 
-  hom-function-Category :
+  hom-set-function-Category :
     obj-function-Category → obj-function-Category → Set (l1 ⊔ l3)
-  hom-function-Category = hom-set-Category function-Category
+  hom-set-function-Category = hom-set-Category function-Category
 
   hom-function-Category :
     obj-function-Category → obj-function-Category → UU (l1 ⊔ l3)
@@ -73,7 +73,7 @@ module _
     associative-comp-hom-Category function-Category
 
   associative-composition-structure-function-Category :
-    associative-composition-structure-Set hom-function-Category
+    associative-composition-structure-Set hom-set-function-Category
   associative-composition-structure-function-Category =
     associative-composition-structure-Category function-Category
 
@@ -96,7 +96,7 @@ module _
 
   is-unital-function-Category :
     is-unital-composition-structure-Set
-      hom-function-Category
+      hom-set-function-Category
       associative-composition-structure-function-Category
   is-unital-function-Category =
     is-unital-composition-structure-Category function-Category

diff --git a/src/category-theory/function-precategories.lagda.md b/src/category-theory/function-precategories.lagda.md
@@ -39,9 +39,9 @@ module _
   obj-function-Precategory : UU (l1 ⊔ l2)
   obj-function-Precategory = obj-Precategory function-Precategory
 
-  hom-function-Precategory :
+  hom-set-function-Precategory :
     obj-function-Precategory → obj-function-Precategory → Set (l1 ⊔ l3)
-  hom-function-Precategory = hom-set-Precategory function-Precategory
+  hom-set-function-Precategory = hom-set-Precategory function-Precategory
 
   hom-function-Precategory :
     obj-function-Precategory → obj-function-Precategory → UU (l1 ⊔ l3)
@@ -65,7 +65,7 @@ module _
     associative-comp-hom-Precategory function-Precategory
 
   associative-composition-structure-function-Precategory :
-    associative-composition-structure-Set hom-function-Precategory
+    associative-composition-structure-Set hom-set-function-Precategory
   associative-composition-structure-function-Precategory =
     associative-composition-structure-Precategory function-Precategory
 
@@ -88,7 +88,7 @@ module _
 
   is-unital-function-Precategory :
     is-unital-composition-structure-Set
-      hom-function-Precategory
+      hom-set-function-Precategory
       associative-composition-structure-function-Precategory
   is-unital-function-Precategory =
     is-unital-composition-structure-Precategory function-Precategory