rename hom-sets to hom-set

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

Hide file tree

Showing 110 changed files with 726 additions and 725 deletions.
diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
@@ -65,10 +65,10 @@ 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
+        ( hom-Large-Precategory C
           ( X)
           ( map-obj-functor-Large-Precategory G Y)) ≃
-        ( type-hom-Large-Precategory D
+        ( hom-Large-Precategory D
           ( map-obj-functor-Large-Precategory F X)
           ( Y))
       naturality-equiv-is-adjoint-pair-Large-Precategory :
@@ -77,8 +77,8 @@ module _
         { X2 : obj-Large-Precategory C l2}
         { Y1 : obj-Large-Precategory D l3}
         { Y2 : obj-Large-Precategory D l4}
-        ( f : type-hom-Large-Precategory C X2 X1)
-        ( g : type-hom-Large-Precategory D Y1 Y2) →
+        ( f : hom-Large-Precategory C X2 X1)
+        ( g : hom-Large-Precategory D Y1 Y2) →
         coherence-square-maps
           ( map-equiv (equiv-is-adjoint-pair-Large-Precategory X1 Y1))
           ( λ h →
@@ -98,8 +98,8 @@ module _
   map-equiv-is-adjoint-pair-Large-Precategory :
     (H : 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)
+    ( hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y)) →
+    ( hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y)
   map-equiv-is-adjoint-pair-Large-Precategory H X Y =
     map-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)
 
@@ -108,17 +108,17 @@ module _
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    ( 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))
+    ( hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y) ≃
+    ( hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y))
   inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
     inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)
 
   map-inv-equiv-is-adjoint-pair-Large-Precategory :
     (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    ( 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))
+    ( hom-Large-Precategory D (map-obj-functor-Large-Precategory F X) Y) →
+    ( hom-Large-Precategory C X (map-obj-functor-Large-Precategory G Y))
   map-inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
     map-inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)
 
@@ -129,8 +129,8 @@ module _
     { X2 : obj-Large-Precategory C l2}
     { Y1 : obj-Large-Precategory D l3}
     { Y2 : obj-Large-Precategory D l4}
-    ( f : type-hom-Large-Precategory C X2 X1)
-    ( g : type-hom-Large-Precategory D Y1 Y2) →
+    ( f : hom-Large-Precategory C X2 X1)
+    ( g : hom-Large-Precategory D Y1 Y2) →
     coherence-square-maps
       ( map-inv-equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
       ( λ h →
@@ -227,8 +227,8 @@ module _
     {l1 l2 : Level}
     {X : obj-Large-Precategory C l1}
     {Y : obj-Large-Precategory C l2} →
-    type-hom-Large-Precategory C X Y →
-    type-hom-Large-Precategory D
+    hom-Large-Precategory C X Y →
+    hom-Large-Precategory D
       ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
       ( obj-left-adjoint-Adjunction-Large-Precategory FG Y)
   hom-left-adjoint-Adjunction-Large-Precategory FG =
@@ -261,8 +261,8 @@ module _
     {l1 l2 : Level}
     {X : obj-Large-Precategory D l1}
     {Y : obj-Large-Precategory D l2} →
-    type-hom-Large-Precategory D X Y →
-    type-hom-Large-Precategory C
+    hom-Large-Precategory D X Y →
+    hom-Large-Precategory C
       ( obj-right-adjoint-Adjunction-Large-Precategory FG X)
       ( obj-right-adjoint-Adjunction-Large-Precategory FG Y)
   hom-right-adjoint-Adjunction-Large-Precategory FG =
@@ -285,10 +285,10 @@ module _
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory C
+    hom-Large-Precategory C
       ( X)
       ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) ≃
-    type-hom-Large-Precategory D
+    hom-Large-Precategory D
       ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
       ( Y)
   equiv-is-adjoint-pair-Adjunction-Large-Precategory FG =
@@ -300,10 +300,10 @@ module _
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory C
+    hom-Large-Precategory C
       ( X)
       ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) →
-    type-hom-Large-Precategory D
+    hom-Large-Precategory D
       ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
       ( Y)
   map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG =
@@ -319,8 +319,8 @@ module _
     {X2 : obj-Large-Precategory C l2}
     {Y1 : obj-Large-Precategory D l3}
     {Y2 : obj-Large-Precategory D l4}
-    (f : type-hom-Large-Precategory C X2 X1)
-    (g : type-hom-Large-Precategory D Y1 Y2) →
+    (f : hom-Large-Precategory C X2 X1)
+    (g : hom-Large-Precategory D Y1 Y2) →
     coherence-square-maps
       ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1)
       ( λ h →
@@ -343,10 +343,10 @@ module _
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    ( type-hom-Large-Precategory D
+    ( hom-Large-Precategory D
       ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
       ( Y)) ≃
-    ( type-hom-Large-Precategory C
+    ( hom-Large-Precategory C
       ( X)
       ( obj-right-adjoint-Adjunction-Large-Precategory FG Y))
   inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y =
@@ -357,10 +357,10 @@ module _
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory D l2) →
-    type-hom-Large-Precategory D
+    hom-Large-Precategory D
       ( obj-left-adjoint-Adjunction-Large-Precategory FG X)
       ( Y) →
-    type-hom-Large-Precategory C
+    hom-Large-Precategory C
       ( X)
       ( obj-right-adjoint-Adjunction-Large-Precategory FG Y)
   map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y =
@@ -373,8 +373,8 @@ module _
     {X2 : obj-Large-Precategory C l2}
     {Y1 : obj-Large-Precategory D l3}
     {Y2 : obj-Large-Precategory D l4}
-    (f : type-hom-Large-Precategory C X2 X1)
-    (g : type-hom-Large-Precategory D Y1 Y2) →
+    (f : hom-Large-Precategory C X2 X1)
+    (g : hom-Large-Precategory D Y1 Y2) →
     coherence-square-maps
       ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1)
       ( λ h →
@@ -489,7 +489,7 @@ module _
     where
     η :
       {l : Level} (X : obj-Large-Precategory C l) →
-      type-hom-Large-Precategory C X
+      hom-Large-Precategory C X
         ( obj-right-adjoint-Adjunction-Large-Precategory C D FG
           ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X))
     η =
@@ -576,7 +576,7 @@ Given an adjoint pair `F ⊣ G`, we can construct a natural transformation
     where
     ε :
       {l : Level} (Y : obj-Large-Precategory D l) →
-      type-hom-Large-Precategory D
+      hom-Large-Precategory D
         ( obj-left-adjoint-Adjunction-Large-Precategory C D FG
           ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y))
         ( Y)

diff --git a/src/category-theory/anafunctors-categories.lagda.md b/src/category-theory/anafunctors-categories.lagda.md
@@ -48,7 +48,7 @@ module _
     (X Y : obj-Category C) (U : obj-Category D)
     (u : object-anafunctor-Category X U)
     (V : obj-Category D) (v : object-anafunctor-Category Y V) →
-    type-hom-Category C X Y → type-hom-Category D U V
+    hom-Category C X Y → hom-Category D U V
   hom-anafunctor-Category =
     hom-anafunctor-Precategory
       ( precategory-Category C)

diff --git a/src/category-theory/anafunctors-precategories.lagda.md b/src/category-theory/anafunctors-precategories.lagda.md
@@ -39,7 +39,7 @@ anafunctor-Precategory l C D =
       Σ ( ( X Y : obj-Precategory C)
           ( U : obj-Precategory D) (u : F₀ X U) →
           ( V : obj-Precategory D) (v : F₀ Y V) →
-          ( f : type-hom-Precategory C X Y) → type-hom-Precategory D U V)
+          ( f : hom-Precategory C X Y) → hom-Precategory D U V)
         ( λ F₁ →
           ( ( X : obj-Precategory C) →
             type-trunc-Prop (Σ (obj-Precategory D) (F₀ X))) ×
@@ -50,8 +50,8 @@ anafunctor-Precategory l C D =
               ( U : obj-Precategory D) (u : F₀ X U)
               ( V : obj-Precategory D) (v : F₀ Y V)
               ( W : obj-Precategory D) (w : F₀ Z W) →
-              ( g : type-hom-Precategory C Y Z)
-              ( f : type-hom-Precategory C X Y) →
+              ( g : hom-Precategory C Y Z)
+              ( f : hom-Precategory C X Y) →
               ( F₁ X Z U u W w (comp-hom-Precategory C g f)) ＝
               ( comp-hom-Precategory D
                 ( F₁ Y Z V v W w g)
@@ -69,7 +69,7 @@ module _
     (X Y : obj-Precategory C)
     (U : obj-Precategory D) (u : object-anafunctor-Precategory X U)
     (V : obj-Precategory D) (v : object-anafunctor-Precategory Y V) →
-    type-hom-Precategory C X Y → type-hom-Precategory D U V
+    hom-Precategory C X Y → hom-Precategory D U V
   hom-anafunctor-Precategory = pr1 (pr2 F)
 ```
 

diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md
@@ -61,54 +61,54 @@ module _
   obj-Category : UU l1
   obj-Category = obj-Precategory precategory-Category
 
-  hom-Category : obj-Category → obj-Category → Set l2
-  hom-Category = hom-Precategory precategory-Category
+  hom-set-Category : obj-Category → obj-Category → Set l2
+  hom-set-Category = hom-set-Precategory precategory-Category
 
-  type-hom-Category : obj-Category → obj-Category → UU l2
-  type-hom-Category = type-hom-Precategory precategory-Category
+  hom-Category : obj-Category → obj-Category → UU l2
+  hom-Category = hom-Precategory precategory-Category
 
-  is-set-type-hom-Category :
-    (x y : obj-Category) → is-set (type-hom-Category x y)
-  is-set-type-hom-Category = is-set-type-hom-Precategory precategory-Category
+  is-set-hom-Category :
+    (x y : obj-Category) → is-set (hom-Category x y)
+  is-set-hom-Category = is-set-hom-Precategory precategory-Category
 
   comp-hom-Category :
     {x y z : obj-Category} →
-    type-hom-Category y z → type-hom-Category x y → type-hom-Category x z
+    hom-Category y z → hom-Category x y → hom-Category x z
   comp-hom-Category = comp-hom-Precategory precategory-Category
 
   associative-comp-hom-Category :
     {x y z w : obj-Category}
-    (h : type-hom-Category z w)
-    (g : type-hom-Category y z)
-    (f : type-hom-Category x y) →
+    (h : hom-Category z w)
+    (g : hom-Category y z)
+    (f : hom-Category x y) →
     comp-hom-Category (comp-hom-Category h g) f ＝
     comp-hom-Category h (comp-hom-Category g f)
   associative-comp-hom-Category =
     associative-comp-hom-Precategory precategory-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-Precategory precategory-Category
 
-  id-hom-Category : {x : obj-Category} → type-hom-Category x x
+  id-hom-Category : {x : obj-Category} → hom-Category x x
   id-hom-Category = id-hom-Precategory precategory-Category
 
   left-unit-law-comp-hom-Category :
-    {x y : obj-Category} (f : type-hom-Category x y) →
+    {x y : obj-Category} (f : hom-Category x y) →
     comp-hom-Category id-hom-Category f ＝ f
   left-unit-law-comp-hom-Category =
     left-unit-law-comp-hom-Precategory precategory-Category
 
   right-unit-law-comp-hom-Category :
-    {x y : obj-Category} (f : type-hom-Category x y) →
+    {x y : obj-Category} (f : hom-Category x y) →
     comp-hom-Category f id-hom-Category ＝ f
   right-unit-law-comp-hom-Category =
     right-unit-law-comp-hom-Precategory precategory-Category
 
   is-unital-composition-structure-Category :
     is-unital-composition-structure-Set
-      hom-Category
+      hom-set-Category
       associative-composition-structure-Category
   is-unital-composition-structure-Category =
     is-unital-composition-structure-Precategory precategory-Category
@@ -123,8 +123,8 @@ module _
 ```agda
 precomp-hom-Category :
   {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
-  (f : type-hom-Category C x y) (z : obj-Category C) →
-  type-hom-Category C y z → type-hom-Category C x z
+  (f : hom-Category C x y) (z : obj-Category C) →
+  hom-Category C y z → hom-Category C x z
 precomp-hom-Category C = precomp-hom-Precategory (precategory-Category C)
 ```
 
@@ -133,8 +133,8 @@ precomp-hom-Category C = precomp-hom-Precategory (precategory-Category C)
 ```agda
 postcomp-hom-Category :
   {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
-  (f : type-hom-Category C x y) (z : obj-Category C) →
-  type-hom-Category C z x → type-hom-Category C z y
+  (f : hom-Category C x y) (z : obj-Category C) →
+  hom-Category C z x → hom-Category C z y
 postcomp-hom-Category C = postcomp-hom-Precategory (precategory-Category C)
 ```
 

diff --git a/src/category-theory/category-of-functors.lagda.md b/src/category-theory/category-of-functors.lagda.md
@@ -48,21 +48,21 @@ module _
       ( precategory-Category C)
       ( precategory-Category D)
 
-  is-category-functor-category-Precategory :
-    is-category-Precategory functor-category-Precategory
-  is-category-functor-category-Precategory F G =
-    is-equiv-htpy-equiv
-      ( equiv-iso-functor-natural-isomorphism-Precategory
-        ( precategory-Category C)
-        ( precategory-Category D)
-        ( F)
-        ( G) ∘e
-        {!  !} ∘e
-        ( extensionality-functor-Category' C D F G))
-      {!   !}
+  -- is-category-functor-category-Precategory :
+  --   is-category-Precategory functor-category-Precategory
+  -- is-category-functor-category-Precategory F G =
+  --   is-equiv-htpy-equiv
+  --     ( equiv-iso-functor-natural-isomorphism-Precategory
+  --       ( precategory-Category C)
+  --       ( precategory-Category D)
+  --       ( F)
+  --       ( G) ∘e
+  --       {!  !} ∘e
+  --       ( extensionality-functor-Category' C D F G))
+  --     {!   !}
 
-  functor-category-Category :
-    Category (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l2 ⊔ l4)
-  pr1 functor-category-Category = functor-category-Precategory
-  pr2 functor-category-Category = is-category-functor-category-Precategory
+  -- functor-category-Category :
+  --   Category (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l2 ⊔ l4)
+  -- pr1 functor-category-Category = functor-category-Precategory
+  -- pr2 functor-category-Category = is-category-functor-category-Precategory
 ```