From 3a646ce58cc0b07256330d4fd150f7816aaa1cca Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 21 Sep 2023 22:53:24 +0200 Subject: [PATCH] fix hom-set function categories --- .../dependent-products-of-categories.lagda.md | 8 ++++---- .../dependent-products-of-precategories.lagda.md | 13 +++++++------ src/category-theory/function-categories.lagda.md | 8 ++++---- src/category-theory/function-precategories.lagda.md | 8 ++++---- 4 files changed, 19 insertions(+), 18 deletions(-) diff --git a/src/category-theory/dependent-products-of-categories.lagda.md b/src/category-theory/dependent-products-of-categories.lagda.md index fc14204ebe..a058b4818d 100644 --- 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 index 2b9532eefa..a8b4f6e35e 100644 --- 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,7 +87,7 @@ 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 @@ -94,7 +95,7 @@ module _ Π-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 index 0ad3435852..6f5545d87c 100644 --- 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 index c6dc631914..283afa77be 100644 --- 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