diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
index 83eef0322c..5dba854aac 100644
--- 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,8 +108,8 @@ 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)
 
@@ -117,8 +117,8 @@ module _
     (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
index 4cc6b74fba..447086f3eb 100644
--- 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
index 929d1577f4..b92eb944ba 100644
--- 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
index 934d145fc2..2e5021b45e 100644
--- 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
index 35b9aad60b..d26e39ad81 100644
--- 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
 ```
diff --git a/src/category-theory/coproducts-in-precategories.lagda.md b/src/category-theory/coproducts-in-precategories.lagda.md
index 94c6e6b8e7..1eb5e2e64e 100644
--- a/src/category-theory/coproducts-in-precategories.lagda.md
+++ b/src/category-theory/coproducts-in-precategories.lagda.md
@@ -33,13 +33,13 @@ module _
 
   is-coproduct-Precategory :
     (x y p : obj-Precategory C) →
-    type-hom-Precategory C x p → type-hom-Precategory C y p → UU (l1 ⊔ l2)
+    hom-Precategory C x p → hom-Precategory C y p → UU (l1 ⊔ l2)
   is-coproduct-Precategory x y p l r =
     (z : obj-Precategory C)
-    (f : type-hom-Precategory C x z) →
-    (g : type-hom-Precategory C y z) →
+    (f : hom-Precategory C x z) →
+    (g : hom-Precategory C y z) →
     ∃!
-      ( type-hom-Precategory C p z)
+      ( hom-Precategory C p z)
       ( λ h →
         ( comp-hom-Precategory C h l ＝ f) ×
         ( comp-hom-Precategory C h r ＝ g))
@@ -48,9 +48,9 @@ module _
   coproduct-Precategory x y =
     Σ ( obj-Precategory C)
       ( λ p →
-        Σ ( type-hom-Precategory C x p)
+        Σ ( hom-Precategory C x p)
           ( λ l →
-            Σ (type-hom-Precategory C y p)
+            Σ (hom-Precategory C y p)
               ( is-coproduct-Precategory x y p l)))
 
   has-all-binary-coproducts : UU (l1 ⊔ l2)
@@ -67,23 +67,23 @@ module _
 
   inl-coproduct-Precategory :
     (x y : obj-Precategory C) →
-    type-hom-Precategory C x (object-coproduct-Precategory x y)
+    hom-Precategory C x (object-coproduct-Precategory x y)
   inl-coproduct-Precategory x y = pr1 (pr2 (t x y))
 
   inr-coproduct-Precategory :
     (x y : obj-Precategory C) →
-    type-hom-Precategory C y (object-coproduct-Precategory x y)
+    hom-Precategory C y (object-coproduct-Precategory x y)
   inr-coproduct-Precategory x y =
     pr1 (pr2 (pr2 (t x y)))
 
   module _
     (x y z : obj-Precategory C)
-    (f : type-hom-Precategory C x z)
-    (g : type-hom-Precategory C y z)
+    (f : hom-Precategory C x z)
+    (g : hom-Precategory C y z)
     where
 
     morphism-out-of-coproduct-Precategory :
-      type-hom-Precategory C (object-coproduct-Precategory x y) z
+      hom-Precategory C (object-coproduct-Precategory x y) z
     morphism-out-of-coproduct-Precategory =
       pr1 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g))
 
@@ -104,7 +104,7 @@ module _
       pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g)))
 
     is-unique-morphism-out-of-coproduct-Precategory :
-      (h : type-hom-Precategory C (object-coproduct-Precategory x y) z) →
+      (h : hom-Precategory C (object-coproduct-Precategory x y) z) →
       comp-hom-Precategory C h (inl-coproduct-Precategory x y) ＝ f →
       comp-hom-Precategory C h (inr-coproduct-Precategory x y) ＝ g →
       morphism-out-of-coproduct-Precategory ＝ h
@@ -114,8 +114,8 @@ module _
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   (x y p : obj-Precategory C)
-  (l : type-hom-Precategory C x p)
-  (r : type-hom-Precategory C y p)
+  (l : hom-Precategory C x p)
+  (r : hom-Precategory C y p)
   where
 
   is-prop-is-coproduct-Precategory :
@@ -144,12 +144,12 @@ module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   (t : has-all-binary-coproducts C)
   {x₁ x₂ y₁ y₂ : obj-Precategory C}
-  (f : type-hom-Precategory C x₁ y₁)
-  (g : type-hom-Precategory C x₂ y₂)
+  (f : hom-Precategory C x₁ y₁)
+  (g : hom-Precategory C x₂ y₂)
   where
 
   map-coproduct-Precategory :
-    type-hom-Precategory C
+    hom-Precategory C
       (object-coproduct-Precategory C t x₁ x₂)
       (object-coproduct-Precategory C t y₁ y₂)
   map-coproduct-Precategory =
diff --git a/src/category-theory/dependent-products-of-categories.lagda.md b/src/category-theory/dependent-products-of-categories.lagda.md
index f0141d233e..fc14204ebe 100644
--- a/src/category-theory/dependent-products-of-categories.lagda.md
+++ b/src/category-theory/dependent-products-of-categories.lagda.md
@@ -61,24 +61,24 @@ module _
 
   hom-Π-Category :
     obj-Π-Category → obj-Π-Category → Set (l1 ⊔ l3)
-  hom-Π-Category = hom-Category Π-Category
+  hom-Π-Category = hom-set-Category Π-Category
 
-  type-hom-Π-Category :
+  hom-Π-Category :
     obj-Π-Category → obj-Π-Category → UU (l1 ⊔ l3)
-  type-hom-Π-Category = type-hom-Category Π-Category
+  hom-Π-Category = hom-Category Π-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-Category Π-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 =
@@ -90,18 +90,18 @@ module _
     associative-composition-structure-Category Π-Category
 
   id-hom-Π-Category :
-    {x : obj-Π-Category} → type-hom-Π-Category x x
+    {x : obj-Π-Category} → hom-Π-Category x x
   id-hom-Π-Category = id-hom-Category Π-Category
 
   left-unit-law-comp-hom-Π-Category :
     {x y : obj-Π-Category}
-    (f : type-hom-Π-Category x y) →
+    (f : hom-Π-Category x y) →
     comp-hom-Π-Category id-hom-Π-Category f ＝ f
   left-unit-law-comp-hom-Π-Category =
     left-unit-law-comp-hom-Category Π-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-Category Π-Category
@@ -128,7 +128,7 @@ module _
   where
 
   is-fiberwise-iso-is-iso-Π-Category :
-    (f : type-hom-Π-Category I C x y) →
+    (f : hom-Π-Category I C x y) →
     is-iso-hom-Category (Π-Category I C) f →
     (i : I) → is-iso-hom-Category (C i) (f i)
   is-fiberwise-iso-is-iso-Π-Category =
@@ -141,7 +141,7 @@ module _
     fiberwise-iso-iso-Π-Precategory I (precategory-Category ∘ C)
 
   is-iso-Π-is-fiberwise-iso-Category :
-    (f : type-hom-Π-Category I C x y) →
+    (f : hom-Π-Category I C x y) →
     ((i : I) → is-iso-hom-Category (C i) (f i)) →
     is-iso-hom-Category (Π-Category I C) f
   is-iso-Π-is-fiberwise-iso-Category =
@@ -154,26 +154,26 @@ module _
     iso-Π-fiberwise-iso-Precategory I (precategory-Category ∘ C)
 
   is-equiv-is-fiberwise-iso-is-iso-Π-Category :
-    (f : type-hom-Π-Category I C x y) →
+    (f : hom-Π-Category I C x y) →
     is-equiv (is-fiberwise-iso-is-iso-Π-Category f)
   is-equiv-is-fiberwise-iso-is-iso-Π-Category =
     is-equiv-is-fiberwise-iso-is-iso-Π-Precategory I (precategory-Category ∘ C)
 
   equiv-is-fiberwise-iso-is-iso-Π-Category :
-    (f : type-hom-Π-Category I C x y) →
+    (f : hom-Π-Category I C x y) →
     ( is-iso-hom-Category (Π-Category I C) f) ≃
     ( (i : I) → is-iso-hom-Category (C i) (f i))
   equiv-is-fiberwise-iso-is-iso-Π-Category =
     equiv-is-fiberwise-iso-is-iso-Π-Precategory I (precategory-Category ∘ C)
 
   is-equiv-is-iso-Π-is-fiberwise-iso-Category :
-    (f : type-hom-Π-Category I C x y) →
+    (f : hom-Π-Category I C x y) →
     is-equiv (is-iso-Π-is-fiberwise-iso-Category f)
   is-equiv-is-iso-Π-is-fiberwise-iso-Category =
     is-equiv-is-iso-Π-is-fiberwise-iso-Precategory I (precategory-Category ∘ C)
 
   equiv-is-iso-Π-is-fiberwise-iso-Category :
-    ( f : type-hom-Π-Category I C x y) →
+    ( f : hom-Π-Category I C x y) →
     ( (i : I) → is-iso-hom-Category (C i) (f i)) ≃
     ( is-iso-hom-Category (Π-Category I C) f)
   equiv-is-iso-Π-is-fiberwise-iso-Category =
diff --git a/src/category-theory/dependent-products-of-precategories.lagda.md b/src/category-theory/dependent-products-of-precategories.lagda.md
index 3886757cc8..2b9532eefa 100644
--- a/src/category-theory/dependent-products-of-precategories.lagda.md
+++ b/src/category-theory/dependent-products-of-precategories.lagda.md
@@ -40,23 +40,23 @@ module _
   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-Precategory (C i) (x i) (y i))
+  hom-Π-Precategory x y = Π-Set' I (λ i → hom-set-Precategory (C i) (x i) (y i))
 
-  type-hom-Π-Precategory : obj-Π-Precategory → obj-Π-Precategory → UU (l1 ⊔ l3)
-  type-hom-Π-Precategory x y = type-Set (hom-Π-Precategory x y)
+  hom-Π-Precategory : obj-Π-Precategory → obj-Π-Precategory → UU (l1 ⊔ l3)
+  hom-Π-Precategory x y = type-Set (hom-Π-Precategory x y)
 
   comp-hom-Π-Precategory :
     {x y z : obj-Π-Precategory} →
-    type-hom-Π-Precategory y z →
-    type-hom-Π-Precategory x y →
-    type-hom-Π-Precategory x z
+    hom-Π-Precategory y z →
+    hom-Π-Precategory x y →
+    hom-Π-Precategory x z
   comp-hom-Π-Precategory f g i = comp-hom-Precategory (C i) (f i) (g i)
 
   associative-comp-hom-Π-Precategory :
     {x y z w : obj-Π-Precategory}
-    (h : type-hom-Π-Precategory z w)
-    (g : type-hom-Π-Precategory y z)
-    (f : type-hom-Π-Precategory x y) →
+    (h : hom-Π-Precategory z w)
+    (g : hom-Π-Precategory y z)
+    (f : hom-Π-Precategory x y) →
     ( comp-hom-Π-Precategory (comp-hom-Π-Precategory h g) f) ＝
     ( comp-hom-Π-Precategory h (comp-hom-Π-Precategory g f))
   associative-comp-hom-Π-Precategory h g f =
@@ -68,18 +68,18 @@ module _
   pr2 associative-composition-structure-Π-Precategory =
     associative-comp-hom-Π-Precategory
 
-  id-hom-Π-Precategory : {x : obj-Π-Precategory} → type-hom-Π-Precategory x x
+  id-hom-Π-Precategory : {x : obj-Π-Precategory} → hom-Π-Precategory x x
   id-hom-Π-Precategory i = id-hom-Precategory (C i)
 
   left-unit-law-comp-hom-Π-Precategory :
     {x y : obj-Π-Precategory}
-    (f : type-hom-Π-Precategory x y) →
+    (f : hom-Π-Precategory x y) →
     comp-hom-Π-Precategory id-hom-Π-Precategory f ＝ f
   left-unit-law-comp-hom-Π-Precategory f =
     eq-htpy (λ i → left-unit-law-comp-hom-Precategory (C i) (f i))
 
   right-unit-law-comp-hom-Π-Precategory :
-    {x y : obj-Π-Precategory} (f : type-hom-Π-Precategory x y) →
+    {x y : obj-Π-Precategory} (f : hom-Π-Precategory x y) →
     comp-hom-Π-Precategory f id-hom-Π-Precategory ＝ f
   right-unit-law-comp-hom-Π-Precategory f =
     eq-htpy (λ i → right-unit-law-comp-hom-Precategory (C i) (f i))
@@ -111,7 +111,7 @@ module _
   where
 
   is-fiberwise-iso-is-iso-Π-Precategory :
-    (f : type-hom-Π-Precategory I C x y) →
+    (f : hom-Π-Precategory I C x y) →
     is-iso-hom-Precategory (Π-Precategory I C) f →
     (i : I) → is-iso-hom-Precategory (C i) (f i)
   pr1 (is-fiberwise-iso-is-iso-Π-Precategory f is-iso-f i) =
@@ -139,7 +139,7 @@ module _
       ( i)
 
   is-iso-Π-is-fiberwise-iso-Precategory :
-    (f : type-hom-Π-Precategory I C x y) →
+    (f : hom-Π-Precategory I C x y) →
     ((i : I) → is-iso-hom-Precategory (C i) (f i)) →
     is-iso-hom-Precategory (Π-Precategory I C) f
   pr1 (is-iso-Π-is-fiberwise-iso-Precategory f is-fiberwise-iso-f) i =
@@ -165,7 +165,7 @@ module _
       ( λ i → is-iso-hom-iso-Precategory (C i) (e i))
 
   is-equiv-is-fiberwise-iso-is-iso-Π-Precategory :
-    (f : type-hom-Π-Precategory I C x y) →
+    (f : hom-Π-Precategory I C x y) →
     is-equiv (is-fiberwise-iso-is-iso-Π-Precategory f)
   is-equiv-is-fiberwise-iso-is-iso-Π-Precategory f =
     is-equiv-is-prop
@@ -174,7 +174,7 @@ module _
       ( is-iso-Π-is-fiberwise-iso-Precategory f)
 
   equiv-is-fiberwise-iso-is-iso-Π-Precategory :
-    (f : type-hom-Π-Precategory I C x y) →
+    (f : hom-Π-Precategory I C x y) →
     ( is-iso-hom-Precategory (Π-Precategory I C) f) ≃
     ( (i : I) → is-iso-hom-Precategory (C i) (f i))
   pr1 (equiv-is-fiberwise-iso-is-iso-Π-Precategory f) =
@@ -183,7 +183,7 @@ module _
     is-equiv-is-fiberwise-iso-is-iso-Π-Precategory f
 
   is-equiv-is-iso-Π-is-fiberwise-iso-Precategory :
-    (f : type-hom-Π-Precategory I C x y) →
+    (f : hom-Π-Precategory I C x y) →
     is-equiv (is-iso-Π-is-fiberwise-iso-Precategory f)
   is-equiv-is-iso-Π-is-fiberwise-iso-Precategory f =
     is-equiv-is-prop
@@ -192,7 +192,7 @@ module _
       ( is-fiberwise-iso-is-iso-Π-Precategory f)
 
   equiv-is-iso-Π-is-fiberwise-iso-Precategory :
-    ( f : type-hom-Π-Precategory I C x y) →
+    ( f : hom-Π-Precategory I C x y) →
     ( (i : I) → is-iso-hom-Precategory (C i) (f i)) ≃
     ( is-iso-hom-Precategory (Π-Precategory I C) f)
   pr1 (equiv-is-iso-Π-is-fiberwise-iso-Precategory f) =
diff --git a/src/category-theory/endomorphisms-in-precategories.lagda.md b/src/category-theory/endomorphisms-in-precategories.lagda.md
index 5af144e13d..75cac02bde 100644
--- a/src/category-theory/endomorphisms-in-precategories.lagda.md
+++ b/src/category-theory/endomorphisms-in-precategories.lagda.md
@@ -30,7 +30,7 @@ module _
   where
 
   type-endo-Precategory : UU l2
-  type-endo-Precategory = type-hom-Precategory C X X
+  type-endo-Precategory = hom-Precategory C X X
 
   comp-endo-Precategory :
     type-endo-Precategory → type-endo-Precategory → type-endo-Precategory
@@ -56,7 +56,7 @@ module _
   right-unit-law-comp-endo-Precategory = right-unit-law-comp-hom-Precategory C
 
   set-endo-Precategory : Set l2
-  set-endo-Precategory = hom-Precategory C X X
+  set-endo-Precategory = hom-set-Precategory C X X
 
   semigroup-endo-Precategory : Semigroup l2
   pr1 semigroup-endo-Precategory = set-endo-Precategory
diff --git a/src/category-theory/epimorphisms-in-large-precategories.lagda.md b/src/category-theory/epimorphisms-in-large-precategories.lagda.md
index 6766641d4f..a9fed314c8 100644
--- a/src/category-theory/epimorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/epimorphisms-in-large-precategories.lagda.md
@@ -34,7 +34,7 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
   (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
-  (f : type-hom-Large-Precategory C X Y)
+  (f : hom-Large-Precategory C X Y)
   where
 
   is-epi-Large-Precategory-Prop : Prop (α l3 ⊔ β l1 l3 ⊔ β l2 l3)
@@ -95,10 +95,10 @@ module _
                     ( right-unit-law-comp-hom-Large-Precategory C h)))))))
       ( λ p →
         eq-is-prop
-          ( is-set-type-hom-Large-Precategory C X Z
+          ( is-set-hom-Large-Precategory C X Z
             ( comp-hom-Large-Precategory C g
               ( hom-iso-Large-Precategory C f))
             ( comp-hom-Large-Precategory C h
               ( hom-iso-Large-Precategory C f))))
-      ( λ p → eq-is-prop (is-set-type-hom-Large-Precategory C Y Z g h))
+      ( λ p → eq-is-prop (is-set-hom-Large-Precategory C Y Z g h))
 ```
diff --git a/src/category-theory/exponential-objects-precategories.lagda.md b/src/category-theory/exponential-objects-precategories.lagda.md
index 0c43763464..80916eb1d8 100644
--- a/src/category-theory/exponential-objects-precategories.lagda.md
+++ b/src/category-theory/exponential-objects-precategories.lagda.md
@@ -42,13 +42,13 @@ module _
 
   is-exponential-Precategory :
     (x y e : obj-Precategory C) →
-    type-hom-Precategory C (object-product-Precategory C p e x) y →
+    hom-Precategory C (object-product-Precategory C p e x) y →
     UU (l1 ⊔ l2)
   is-exponential-Precategory x y e ev =
     (z : obj-Precategory C)
-    (f : type-hom-Precategory C (object-product-Precategory C p z x) y) →
+    (f : hom-Precategory C (object-product-Precategory C p z x) y) →
     ∃!
-      ( type-hom-Precategory C z e)
+      ( hom-Precategory C z e)
       ( λ g →
         comp-hom-Precategory C ev
           ( map-product-Precategory C p g (id-hom-Precategory C)) ＝
@@ -58,7 +58,7 @@ module _
     obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
   exponential-Precategory x y =
     Σ (obj-Precategory C) (λ e →
-    Σ (type-hom-Precategory C (object-product-Precategory C p e x) y) λ ev →
+    Σ (hom-Precategory C (object-product-Precategory C p e x) y) λ ev →
       is-exponential-Precategory x y e ev)
 
   has-all-exponentials-Precategory : UU (l1 ⊔ l2)
@@ -76,18 +76,18 @@ module _
   object-exponential-Precategory = pr1 (t x y)
 
   eval-exponential-Precategory :
-    type-hom-Precategory C
+    hom-Precategory C
       ( object-product-Precategory C p object-exponential-Precategory x)
       ( y)
   eval-exponential-Precategory = pr1 (pr2 (t x y))
 
   module _
     (z : obj-Precategory C)
-    (f : type-hom-Precategory C (object-product-Precategory C p z x) y)
+    (f : hom-Precategory C (object-product-Precategory C p z x) y)
     where
 
     morphism-into-exponential-Precategory :
-      type-hom-Precategory C z object-exponential-Precategory
+      hom-Precategory C z object-exponential-Precategory
     morphism-into-exponential-Precategory = pr1 (pr1 (pr2 (pr2 (t x y)) z f))
 
     morphism-into-exponential-Precategory-comm :
@@ -101,7 +101,7 @@ module _
       pr2 (pr1 (pr2 (pr2 (t x y)) z f))
 
     is-unique-morphism-into-exponential-Precategory :
-      ( g : type-hom-Precategory C z object-exponential-Precategory) →
+      ( g : hom-Precategory C z object-exponential-Precategory) →
       ( comp-hom-Precategory C
         ( eval-exponential-Precategory)
         ( map-product-Precategory C p g (id-hom-Precategory C)) ＝ f) →
diff --git a/src/category-theory/function-categories.lagda.md b/src/category-theory/function-categories.lagda.md
index 718cc18fdc..0ad3435852 100644
--- a/src/category-theory/function-categories.lagda.md
+++ b/src/category-theory/function-categories.lagda.md
@@ -49,24 +49,24 @@ module _
 
   hom-function-Category :
     obj-function-Category → obj-function-Category → Set (l1 ⊔ l3)
-  hom-function-Category = hom-Category function-Category
+  hom-function-Category = hom-set-Category function-Category
 
-  type-hom-function-Category :
+  hom-function-Category :
     obj-function-Category → obj-function-Category → UU (l1 ⊔ l3)
-  type-hom-function-Category = type-hom-Category function-Category
+  hom-function-Category = hom-Category function-Category
 
   comp-hom-function-Category :
     {x y z : obj-function-Category} →
-    type-hom-function-Category y z →
-    type-hom-function-Category x y →
-    type-hom-function-Category x z
+    hom-function-Category y z →
+    hom-function-Category x y →
+    hom-function-Category x z
   comp-hom-function-Category = comp-hom-Category function-Category
 
   associative-comp-hom-function-Category :
     {x y z w : obj-function-Category}
-    (h : type-hom-function-Category z w)
-    (g : type-hom-function-Category y z)
-    (f : type-hom-function-Category x y) →
+    (h : hom-function-Category z w)
+    (g : hom-function-Category y z)
+    (f : hom-function-Category x y) →
     ( comp-hom-function-Category (comp-hom-function-Category h g) f) ＝
     ( comp-hom-function-Category h (comp-hom-function-Category g f))
   associative-comp-hom-function-Category =
@@ -78,18 +78,18 @@ module _
     associative-composition-structure-Category function-Category
 
   id-hom-function-Category :
-    {x : obj-function-Category} → type-hom-function-Category x x
+    {x : obj-function-Category} → hom-function-Category x x
   id-hom-function-Category = id-hom-Category function-Category
 
   left-unit-law-comp-hom-function-Category :
     {x y : obj-function-Category}
-    (f : type-hom-function-Category x y) →
+    (f : hom-function-Category x y) →
     comp-hom-function-Category id-hom-function-Category f ＝ f
   left-unit-law-comp-hom-function-Category =
     left-unit-law-comp-hom-Category function-Category
 
   right-unit-law-comp-hom-function-Category :
-    {x y : obj-function-Category} (f : type-hom-function-Category x y) →
+    {x y : obj-function-Category} (f : hom-function-Category x y) →
     comp-hom-function-Category f id-hom-function-Category ＝ f
   right-unit-law-comp-hom-function-Category =
     right-unit-law-comp-hom-Category function-Category
@@ -117,7 +117,7 @@ module _
   where
 
   is-fiberwise-iso-is-iso-function-Category :
-    (f : type-hom-function-Category I C x y) →
+    (f : hom-function-Category I C x y) →
     is-iso-hom-Category (function-Category I C) f →
     (i : I) → is-iso-hom-Category C (f i)
   is-fiberwise-iso-is-iso-function-Category =
@@ -130,7 +130,7 @@ module _
     fiberwise-iso-iso-Π-Category I (λ _ → C)
 
   is-iso-function-is-fiberwise-iso-Category :
-    (f : type-hom-function-Category I C x y) →
+    (f : hom-function-Category I C x y) →
     ((i : I) → is-iso-hom-Category C (f i)) →
     is-iso-hom-Category (function-Category I C) f
   is-iso-function-is-fiberwise-iso-Category =
@@ -143,26 +143,26 @@ module _
     iso-Π-fiberwise-iso-Category I (λ _ → C)
 
   is-equiv-is-fiberwise-iso-is-iso-function-Category :
-    (f : type-hom-function-Category I C x y) →
+    (f : hom-function-Category I C x y) →
     is-equiv (is-fiberwise-iso-is-iso-function-Category f)
   is-equiv-is-fiberwise-iso-is-iso-function-Category =
     is-equiv-is-fiberwise-iso-is-iso-Π-Category I (λ _ → C)
 
   equiv-is-fiberwise-iso-is-iso-function-Category :
-    (f : type-hom-function-Category I C x y) →
+    (f : hom-function-Category I C x y) →
     ( is-iso-hom-Category (function-Category I C) f) ≃
     ( (i : I) → is-iso-hom-Category C (f i))
   equiv-is-fiberwise-iso-is-iso-function-Category =
     equiv-is-fiberwise-iso-is-iso-Π-Category I (λ _ → C)
 
   is-equiv-is-iso-function-is-fiberwise-iso-Category :
-    (f : type-hom-function-Category I C x y) →
+    (f : hom-function-Category I C x y) →
     is-equiv (is-iso-function-is-fiberwise-iso-Category f)
   is-equiv-is-iso-function-is-fiberwise-iso-Category =
     is-equiv-is-iso-Π-is-fiberwise-iso-Category I (λ _ → C)
 
   equiv-is-iso-function-is-fiberwise-iso-Category :
-    ( f : type-hom-function-Category I C x y) →
+    ( f : hom-function-Category I C x y) →
     ( (i : I) → is-iso-hom-Category C (f i)) ≃
     ( is-iso-hom-Category (function-Category I C) f)
   equiv-is-iso-function-is-fiberwise-iso-Category =
diff --git a/src/category-theory/function-precategories.lagda.md b/src/category-theory/function-precategories.lagda.md
index 232649d346..c6dc631914 100644
--- a/src/category-theory/function-precategories.lagda.md
+++ b/src/category-theory/function-precategories.lagda.md
@@ -41,24 +41,24 @@ module _
 
   hom-function-Precategory :
     obj-function-Precategory → obj-function-Precategory → Set (l1 ⊔ l3)
-  hom-function-Precategory = hom-Precategory function-Precategory
+  hom-function-Precategory = hom-set-Precategory function-Precategory
 
-  type-hom-function-Precategory :
+  hom-function-Precategory :
     obj-function-Precategory → obj-function-Precategory → UU (l1 ⊔ l3)
-  type-hom-function-Precategory = type-hom-Precategory function-Precategory
+  hom-function-Precategory = hom-Precategory function-Precategory
 
   comp-hom-function-Precategory :
     {x y z : obj-function-Precategory} →
-    type-hom-function-Precategory y z →
-    type-hom-function-Precategory x y →
-    type-hom-function-Precategory x z
+    hom-function-Precategory y z →
+    hom-function-Precategory x y →
+    hom-function-Precategory x z
   comp-hom-function-Precategory = comp-hom-Precategory function-Precategory
 
   associative-comp-hom-function-Precategory :
     {x y z w : obj-function-Precategory}
-    (h : type-hom-function-Precategory z w)
-    (g : type-hom-function-Precategory y z)
-    (f : type-hom-function-Precategory x y) →
+    (h : hom-function-Precategory z w)
+    (g : hom-function-Precategory y z)
+    (f : hom-function-Precategory x y) →
     ( comp-hom-function-Precategory (comp-hom-function-Precategory h g) f) ＝
     ( comp-hom-function-Precategory h (comp-hom-function-Precategory g f))
   associative-comp-hom-function-Precategory =
@@ -70,18 +70,18 @@ module _
     associative-composition-structure-Precategory function-Precategory
 
   id-hom-function-Precategory :
-    {x : obj-function-Precategory} → type-hom-function-Precategory x x
+    {x : obj-function-Precategory} → hom-function-Precategory x x
   id-hom-function-Precategory = id-hom-Precategory function-Precategory
 
   left-unit-law-comp-hom-function-Precategory :
     {x y : obj-function-Precategory}
-    (f : type-hom-function-Precategory x y) →
+    (f : hom-function-Precategory x y) →
     comp-hom-function-Precategory id-hom-function-Precategory f ＝ f
   left-unit-law-comp-hom-function-Precategory =
     left-unit-law-comp-hom-Precategory function-Precategory
 
   right-unit-law-comp-hom-function-Precategory :
-    {x y : obj-function-Precategory} (f : type-hom-function-Precategory x y) →
+    {x y : obj-function-Precategory} (f : hom-function-Precategory x y) →
     comp-hom-function-Precategory f id-hom-function-Precategory ＝ f
   right-unit-law-comp-hom-function-Precategory =
     right-unit-law-comp-hom-Precategory function-Precategory
@@ -103,7 +103,7 @@ module _
   where
 
   is-fiberwise-iso-is-iso-function-Precategory :
-    (f : type-hom-function-Precategory I C x y) →
+    (f : hom-function-Precategory I C x y) →
     is-iso-hom-Precategory (function-Precategory I C) f →
     (i : I) → is-iso-hom-Precategory C (f i)
   is-fiberwise-iso-is-iso-function-Precategory =
@@ -116,7 +116,7 @@ module _
     fiberwise-iso-iso-Π-Precategory I (λ _ → C)
 
   is-iso-function-is-fiberwise-iso-Precategory :
-    (f : type-hom-function-Precategory I C x y) →
+    (f : hom-function-Precategory I C x y) →
     ((i : I) → is-iso-hom-Precategory C (f i)) →
     is-iso-hom-Precategory (function-Precategory I C) f
   is-iso-function-is-fiberwise-iso-Precategory =
@@ -129,26 +129,26 @@ module _
     iso-Π-fiberwise-iso-Precategory I (λ _ → C)
 
   is-equiv-is-fiberwise-iso-is-iso-function-Precategory :
-    (f : type-hom-function-Precategory I C x y) →
+    (f : hom-function-Precategory I C x y) →
     is-equiv (is-fiberwise-iso-is-iso-function-Precategory f)
   is-equiv-is-fiberwise-iso-is-iso-function-Precategory =
     is-equiv-is-fiberwise-iso-is-iso-Π-Precategory I (λ _ → C)
 
   equiv-is-fiberwise-iso-is-iso-function-Precategory :
-    (f : type-hom-function-Precategory I C x y) →
+    (f : hom-function-Precategory I C x y) →
     ( is-iso-hom-Precategory (function-Precategory I C) f) ≃
     ( (i : I) → is-iso-hom-Precategory C (f i))
   equiv-is-fiberwise-iso-is-iso-function-Precategory =
     equiv-is-fiberwise-iso-is-iso-Π-Precategory I (λ _ → C)
 
   is-equiv-is-iso-function-is-fiberwise-iso-Precategory :
-    (f : type-hom-function-Precategory I C x y) →
+    (f : hom-function-Precategory I C x y) →
     is-equiv (is-iso-function-is-fiberwise-iso-Precategory f)
   is-equiv-is-iso-function-is-fiberwise-iso-Precategory =
     is-equiv-is-iso-Π-is-fiberwise-iso-Precategory I (λ _ → C)
 
   equiv-is-iso-function-is-fiberwise-iso-Precategory :
-    ( f : type-hom-function-Precategory I C x y) →
+    ( f : hom-function-Precategory I C x y) →
     ( (i : I) → is-iso-hom-Precategory C (f i)) ≃
     ( is-iso-hom-Precategory (function-Precategory I C) f)
   equiv-is-iso-function-is-fiberwise-iso-Precategory =
diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
index 5ff7a9b92d..d040adfbbb 100644
--- a/src/category-theory/functors-categories.lagda.md
+++ b/src/category-theory/functors-categories.lagda.md
@@ -50,8 +50,8 @@ module _
   map-hom-map-Category :
     (F : map-Category)
     {x y : obj-Category C} →
-    type-hom-Category C x y →
-    type-hom-Category D
+    hom-Category C x y →
+    hom-Category D
       ( map-obj-map-Category F x)
       ( map-obj-map-Category F y)
   map-hom-map-Category =
@@ -128,8 +128,8 @@ module _
   map-hom-functor-Category :
     (F : functor-Category) →
     {x y : obj-Category C} →
-    (f : type-hom-Category C x y) →
-    type-hom-Category D
+    (f : hom-Category C x y) →
+    hom-Category D
       ( map-obj-functor-Category F x)
       ( map-obj-functor-Category F y)
   map-hom-functor-Category =
@@ -143,7 +143,7 @@ module _
 
   preserves-comp-functor-Category :
     ( F : functor-Category) {x y z : obj-Category C}
-    ( g : type-hom-Category C y z) (f : type-hom-Category C x y) →
+    ( g : hom-Category C y z) (f : hom-Category C x y) →
     ( map-hom-functor-Category F (comp-hom-Category C g f)) ＝
     ( comp-hom-Category D
       ( map-hom-functor-Category F g)
diff --git a/src/category-theory/functors-large-precategories.lagda.md b/src/category-theory/functors-large-precategories.lagda.md
index 4d39978810..87620a7d6e 100644
--- a/src/category-theory/functors-large-precategories.lagda.md
+++ b/src/category-theory/functors-large-precategories.lagda.md
@@ -47,8 +47,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
           ( map-obj-functor-Large-Precategory X)
           ( map-obj-functor-Large-Precategory Y)
       preserves-comp-functor-Large-Precategory :
@@ -56,8 +56,8 @@ module _
         { X : obj-Large-Precategory C l1}
         { Y : obj-Large-Precategory C l2}
         { Z : obj-Large-Precategory C l3}
-        ( g : type-hom-Large-Precategory C Y Z)
-        ( f : type-hom-Large-Precategory C X Y) →
+        ( g : hom-Large-Precategory C Y Z)
+        ( f : hom-Large-Precategory C X Y) →
         ( map-hom-functor-Large-Precategory
           ( comp-hom-Large-Precategory C g f)) ＝
         ( comp-hom-Large-Precategory D
diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md
index adf38a65bb..12309b608a 100644
--- a/src/category-theory/functors-precategories.lagda.md
+++ b/src/category-theory/functors-precategories.lagda.md
@@ -7,7 +7,7 @@ module category-theory.functors-precategories where
 <details><summary>Imports</summary>
 
 ```agda
-open import category-theory.maps-of-categories
+open import category-theory.maps-precategories
 open import category-theory.precategories
 
 open import foundation.action-on-identifications-functions
@@ -54,7 +54,7 @@ module _
   preserves-comp-hom-map-Precategory : UU (l1 ⊔ l2 ⊔ l4)
   preserves-comp-hom-map-Precategory =
     {x y z : obj-Precategory C}
-    (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) →
     ( map-hom-map-Precategory C D F (comp-hom-Precategory C g f)) ＝
     ( comp-hom-Precategory D
       ( map-hom-map-Precategory C D F g)
@@ -94,8 +94,8 @@ module _
     Σ ( obj-Precategory C → obj-Precategory D)
       ( λ F₀ →
         Σ ( {x y : obj-Precategory C}
-            (f : type-hom-Precategory C x y) →
-            type-hom-Precategory D (F₀ x) (F₀ y))
+            (f : hom-Precategory C x y) →
+            hom-Precategory D (F₀ x) (F₀ y))
           ( λ F₁ → is-functor-map-Precategory C D (F₀ , F₁)))
 
   map-obj-functor-Precategory :
@@ -105,8 +105,8 @@ module _
   map-hom-functor-Precategory :
     (F : functor-Precategory) →
     {x y : obj-Precategory C} →
-    (f : type-hom-Precategory C x y) →
-    type-hom-Precategory D
+    (f : hom-Precategory C x y) →
+    hom-Precategory D
       ( map-obj-functor-Precategory F x)
       ( map-obj-functor-Precategory F y)
   map-hom-functor-Precategory F = pr1 (pr2 F)
@@ -117,7 +117,7 @@ module _
 
   preserves-comp-functor-Precategory :
     (F : functor-Precategory) {x y z : obj-Precategory C}
-    (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) →
     ( map-hom-functor-Precategory F (comp-hom-Precategory C g f)) ＝
     ( comp-hom-Precategory D
       ( map-hom-functor-Precategory F g)
@@ -202,7 +202,7 @@ module _
                   ( λ g →
                     is-prop-Π
                       ( λ f →
-                        is-set-type-hom-Precategory D
+                        is-set-hom-Precategory D
                           ( map-obj-map-Precategory C D F x)
                           ( map-obj-map-Precategory C D F z)
                           ( map-hom-map-Precategory C D F
@@ -222,7 +222,7 @@ module _
   is-prop-preserves-id-hom-map-Precategory =
     is-prop-Π
       ( λ x →
-        is-set-type-hom-Precategory D
+        is-set-hom-Precategory D
           ( map-obj-map-Precategory C D F x)
           ( map-obj-map-Precategory C D F x)
           ( map-hom-map-Precategory C D F (id-hom-Precategory C {x}))
@@ -267,8 +267,8 @@ module _
             ( obj-Precategory C → obj-Precategory D)
             ( λ F₀ →
               { x y : obj-Precategory C} →
-              type-hom-Precategory C x y →
-              type-hom-Precategory D (F₀ x) (F₀ y))
+              hom-Precategory C x y →
+              hom-Precategory D (F₀ x) (F₀ y))
             ( pr1 ∘ is-functor-map-Precategory-Prop C D))))
 ```
 
diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md
index 9125285f4a..87e0a98386 100644
--- a/src/category-theory/groupoids.lagda.md
+++ b/src/category-theory/groupoids.lagda.md
@@ -63,37 +63,37 @@ module _
   obj-Groupoid : UU l1
   obj-Groupoid = obj-Category category-Groupoid
 
-  hom-Groupoid : obj-Groupoid → obj-Groupoid → Set l2
-  hom-Groupoid = hom-Category category-Groupoid
+  hom-set-Groupoid : obj-Groupoid → obj-Groupoid → Set l2
+  hom-set-Groupoid = hom-set-Category category-Groupoid
 
-  type-hom-Groupoid : obj-Groupoid → obj-Groupoid → UU l2
-  type-hom-Groupoid = type-hom-Category category-Groupoid
+  hom-Groupoid : obj-Groupoid → obj-Groupoid → UU l2
+  hom-Groupoid = hom-Category category-Groupoid
 
   id-hom-Groupoid :
-    {x : obj-Groupoid} → type-hom-Groupoid x x
+    {x : obj-Groupoid} → hom-Groupoid x x
   id-hom-Groupoid = id-hom-Category category-Groupoid
 
   comp-hom-Groupoid :
-    {x y z : obj-Groupoid} → type-hom-Groupoid y z →
-    type-hom-Groupoid x y → type-hom-Groupoid x z
+    {x y z : obj-Groupoid} → hom-Groupoid y z →
+    hom-Groupoid x y → hom-Groupoid x z
   comp-hom-Groupoid = comp-hom-Category category-Groupoid
 
   associative-comp-hom-Groupoid :
-    {x y z w : obj-Groupoid} (h : type-hom-Groupoid z w)
-    (g : type-hom-Groupoid y z) (f : type-hom-Groupoid x y) →
+    {x y z w : obj-Groupoid} (h : hom-Groupoid z w)
+    (g : hom-Groupoid y z) (f : hom-Groupoid x y) →
     ( comp-hom-Groupoid (comp-hom-Groupoid h g) f) ＝
     ( comp-hom-Groupoid h (comp-hom-Groupoid g f))
   associative-comp-hom-Groupoid =
     associative-comp-hom-Category category-Groupoid
 
   left-unit-law-comp-hom-Groupoid :
-    {x y : obj-Groupoid} (f : type-hom-Groupoid x y) →
+    {x y : obj-Groupoid} (f : hom-Groupoid x y) →
     ( comp-hom-Groupoid id-hom-Groupoid f) ＝ f
   left-unit-law-comp-hom-Groupoid =
     left-unit-law-comp-hom-Category category-Groupoid
 
   right-unit-law-comp-hom-Groupoid :
-    {x y : obj-Groupoid} (f : type-hom-Groupoid x y) →
+    {x y : obj-Groupoid} (f : hom-Groupoid x y) →
     ( comp-hom-Groupoid f id-hom-Groupoid) ＝ f
   right-unit-law-comp-hom-Groupoid =
     right-unit-law-comp-hom-Category category-Groupoid
diff --git a/src/category-theory/initial-objects-large-precategories.lagda.md b/src/category-theory/initial-objects-large-precategories.lagda.md
index 5cdcc662f8..c49900291d 100644
--- a/src/category-theory/initial-objects-large-precategories.lagda.md
+++ b/src/category-theory/initial-objects-large-precategories.lagda.md
@@ -35,5 +35,5 @@ module _
   is-initial-obj-Large-Precategory : UUω
   is-initial-obj-Large-Precategory =
     {l2 : Level} (Y : obj-Large-Precategory C l2) →
-    is-contr (type-hom-Large-Precategory C X Y)
+    is-contr (hom-Large-Precategory C X Y)
 ```
diff --git a/src/category-theory/initial-objects-precategories.lagda.md b/src/category-theory/initial-objects-precategories.lagda.md
index 99c381a7f8..dac1af8fa9 100644
--- a/src/category-theory/initial-objects-precategories.lagda.md
+++ b/src/category-theory/initial-objects-precategories.lagda.md
@@ -39,7 +39,7 @@ module _
   is-initial-prop-obj-Precategory =
     Π-Prop
       ( obj-Precategory C)
-      ( λ y → is-contr-Prop (type-hom-Precategory C x y))
+      ( λ y → is-contr-Prop (hom-Precategory C x y))
 
   is-initial-obj-Precategory : UU (l1 ⊔ l2)
   is-initial-obj-Precategory = type-Prop is-initial-prop-obj-Precategory
@@ -56,12 +56,12 @@ module _
 
   hom-is-initial-obj-Precategory :
     (y : obj-Precategory C) →
-    type-hom-Precategory C x y
+    hom-Precategory C x y
   hom-is-initial-obj-Precategory = center ∘ t
 
   is-unique-hom-is-initial-obj-Precategory :
     (y : obj-Precategory C) →
-    (f : type-hom-Precategory C x y) →
+    (f : hom-Precategory C x y) →
     hom-is-initial-obj-Precategory y ＝ f
   is-unique-hom-is-initial-obj-Precategory = contraction ∘ t
 ```
@@ -89,7 +89,7 @@ module _
 
   hom-initial-obj-Precategory :
     (y : obj-Precategory C) →
-    type-hom-Precategory C obj-initial-obj-Precategory y
+    hom-Precategory C obj-initial-obj-Precategory y
   hom-initial-obj-Precategory =
     hom-is-initial-obj-Precategory C
       ( obj-initial-obj-Precategory)
@@ -97,7 +97,7 @@ module _
 
   is-unique-hom-initial-obj-Precategory :
     (y : obj-Precategory C) →
-    (f : type-hom-Precategory C obj-initial-obj-Precategory y) →
+    (f : hom-Precategory C obj-initial-obj-Precategory y) →
     hom-initial-obj-Precategory y ＝ f
   is-unique-hom-initial-obj-Precategory =
     is-unique-hom-is-initial-obj-Precategory C
diff --git a/src/category-theory/isomorphisms-in-categories.lagda.md b/src/category-theory/isomorphisms-in-categories.lagda.md
index 26a512f5c0..2847928976 100644
--- a/src/category-theory/isomorphisms-in-categories.lagda.md
+++ b/src/category-theory/isomorphisms-in-categories.lagda.md
@@ -43,7 +43,7 @@ is-iso-hom-Category :
   {l1 l2 : Level}
   (C : Category l1 l2)
   {x y : obj-Category C}
-  (f : type-hom-Category C x y) →
+  (f : hom-Category C x y) →
   UU l2
 is-iso-hom-Category C = is-iso-hom-Precategory (precategory-Category C)
 
@@ -51,11 +51,11 @@ module _
   {l1 l2 : Level}
   (C : Category l1 l2)
   {x y : obj-Category C}
-  {f : type-hom-Category C x y}
+  {f : hom-Category C x y}
   where
 
   hom-inv-is-iso-hom-Category :
-    is-iso-hom-Category C f → type-hom-Category C y x
+    is-iso-hom-Category C f → hom-Category C y x
   hom-inv-is-iso-hom-Category =
     hom-inv-is-iso-hom-Precategory (precategory-Category C)
 
@@ -93,7 +93,7 @@ module _
   (f : iso-Category C x y)
   where
 
-  hom-iso-Category : type-hom-Category C x y
+  hom-iso-Category : hom-Category C x y
   hom-iso-Category = hom-iso-Precategory (precategory-Category C) f
 
   is-iso-hom-iso-Category :
@@ -101,7 +101,7 @@ module _
   is-iso-hom-iso-Category =
     is-iso-hom-iso-Precategory (precategory-Category C) f
 
-  hom-inv-iso-Category : type-hom-Category C y x
+  hom-inv-iso-Category : hom-Category C y x
   hom-inv-iso-Category = hom-inv-iso-Precategory (precategory-Category C) f
 
   is-section-hom-inv-iso-Category :
@@ -178,12 +178,12 @@ module _
   where
 
   is-prop-is-iso-hom-Category :
-    (f : type-hom-Category C x y) → is-prop (is-iso-hom-Category C f)
+    (f : hom-Category C x y) → is-prop (is-iso-hom-Category C f)
   is-prop-is-iso-hom-Category =
     is-prop-is-iso-hom-Precategory (precategory-Category C)
 
   is-iso-prop-hom-Category :
-    (f : type-hom-Category C x y) → Prop l2
+    (f : hom-Category C x y) → Prop l2
   is-iso-prop-hom-Category =
     is-iso-prop-hom-Precategory (precategory-Category C)
 ```
@@ -232,14 +232,14 @@ module _
   {l1 l2 : Level}
   (C : Category l1 l2)
   {x y z : obj-Category C}
-  {g : type-hom-Category C y z}
-  {f : type-hom-Category C x y}
+  {g : hom-Category C y z}
+  {f : hom-Category C x y}
   where
 
   hom-comp-is-iso-hom-Category :
     is-iso-hom-Category C g →
     is-iso-hom-Category C f →
-    type-hom-Category C z x
+    hom-Category C z x
   hom-comp-is-iso-hom-Category =
     hom-comp-is-iso-hom-Precategory (precategory-Category C)
 
@@ -281,7 +281,7 @@ module _
   (f : iso-Category C x y)
   where
 
-  hom-comp-iso-Category : type-hom-Category C x z
+  hom-comp-iso-Category : hom-Category C x z
   hom-comp-iso-Category = hom-comp-iso-Precategory (precategory-Category C) g f
 
   is-iso-comp-iso-Category :
@@ -292,7 +292,7 @@ module _
   comp-iso-Category : iso-Category C x z
   comp-iso-Category = comp-iso-Precategory (precategory-Category C) g f
 
-  hom-inv-comp-iso-Category : type-hom-Category C z x
+  hom-inv-comp-iso-Category : hom-Category C z x
   hom-inv-comp-iso-Category =
     hom-inv-comp-iso-Precategory (precategory-Category C) g f
 
@@ -320,7 +320,7 @@ module _
   {l1 l2 : Level}
   (C : Category l1 l2)
   {x y : obj-Category C}
-  {f : type-hom-Category C x y}
+  {f : hom-Category C x y}
   where
 
   is-iso-inv-is-iso-hom-Category :
@@ -443,11 +443,11 @@ module _
   {l1 l2 : Level}
   (C : Category l1 l2)
   {x y : obj-Category C}
-  {f : type-hom-Category C x y}
+  {f : hom-Category C x y}
   (H : (z : obj-Category C) → is-equiv (precomp-hom-Category C f z))
   where
 
-  hom-inv-is-iso-is-equiv-precomp-hom-Category : type-hom-Category C y x
+  hom-inv-is-iso-is-equiv-precomp-hom-Category : hom-Category C y x
   hom-inv-is-iso-is-equiv-precomp-hom-Category =
     hom-inv-is-iso-is-equiv-precomp-hom-Precategory (precategory-Category C) H
 
@@ -508,11 +508,11 @@ module _
   {l1 l2 : Level}
   (C : Category l1 l2)
   {x y : obj-Category C}
-  {f : type-hom-Category C x y}
+  {f : hom-Category C x y}
   (H : (z : obj-Category C) → is-equiv (postcomp-hom-Category C f z))
   where
 
-  hom-inv-is-iso-is-equiv-postcomp-hom-Category : type-hom-Category C y x
+  hom-inv-is-iso-is-equiv-postcomp-hom-Category : hom-Category C y x
   hom-inv-is-iso-is-equiv-postcomp-hom-Category =
     hom-inv-is-iso-is-equiv-postcomp-hom-Precategory (precategory-Category C) H
 
@@ -553,11 +553,11 @@ module _
   where
 
   is-prop-iso-Category :
-    is-prop (type-hom-Category C x y) → is-prop (iso-Category C x y)
+    is-prop (hom-Category C x y) → is-prop (iso-Category C x y)
   is-prop-iso-Category = is-prop-iso-Precategory (precategory-Category C)
 
   iso-prop-Category :
-    is-prop (type-hom-Category C x y) → Prop l2
+    is-prop (hom-Category C x y) → Prop l2
   iso-prop-Category = iso-prop-Precategory (precategory-Category C)
 ```
 
@@ -570,34 +570,34 @@ module _
   where
 
   is-iso-is-prop-hom-Category' :
-    is-prop (type-hom-Category C x x) →
-    is-prop (type-hom-Category C y y) →
-    (f : type-hom-Category C x y) →
-    type-hom-Category C y x →
+    is-prop (hom-Category C x x) →
+    is-prop (hom-Category C y y) →
+    (f : hom-Category C x y) →
+    hom-Category C y x →
     is-iso-hom-Category C f
   is-iso-is-prop-hom-Category' =
     is-iso-is-prop-hom-Precategory' (precategory-Category C)
 
   iso-is-prop-hom-Category' :
-    is-prop (type-hom-Category C x x) →
-    is-prop (type-hom-Category C y y) →
-    type-hom-Category C x y →
-    type-hom-Category C y x →
+    is-prop (hom-Category C x x) →
+    is-prop (hom-Category C y y) →
+    hom-Category C x y →
+    hom-Category C y x →
     iso-Category C x y
   iso-is-prop-hom-Category' =
     iso-is-prop-hom-Precategory' (precategory-Category C)
 
   is-iso-is-prop-hom-Category :
-    ((x' y' : obj-Category C) → is-prop (type-hom-Category C x' y')) →
-    (f : type-hom-Category C x y) → type-hom-Category C y x →
+    ((x' y' : obj-Category C) → is-prop (hom-Category C x' y')) →
+    (f : hom-Category C x y) → hom-Category C y x →
     is-iso-hom-Category C f
   is-iso-is-prop-hom-Category =
     is-iso-is-prop-hom-Precategory (precategory-Category C)
 
   iso-is-prop-hom-Category :
-    ((x' y' : obj-Category C) → is-prop (type-hom-Category C x' y')) →
-    type-hom-Category C x y →
-    type-hom-Category C y x →
+    ((x' y' : obj-Category C) → is-prop (hom-Category C x' y')) →
+    hom-Category C x y →
+    hom-Category C y x →
     iso-Category C x y
   iso-is-prop-hom-Category =
     iso-is-prop-hom-Precategory (precategory-Category C)
diff --git a/src/category-theory/isomorphisms-in-large-categories.lagda.md b/src/category-theory/isomorphisms-in-large-categories.lagda.md
index a3174a1790..dc82d645c5 100644
--- a/src/category-theory/isomorphisms-in-large-categories.lagda.md
+++ b/src/category-theory/isomorphisms-in-large-categories.lagda.md
@@ -38,7 +38,7 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Category α β) {l1 l2 : Level}
   {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
-  (f : type-hom-Large-Category C X Y)
+  (f : hom-Large-Category C X Y)
   where
 
   is-iso-hom-Large-Category : UU (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
@@ -46,7 +46,7 @@ module _
     is-iso-hom-Large-Precategory (large-precategory-Large-Category C) f
 
   hom-inv-is-iso-hom-Large-Category :
-    is-iso-hom-Large-Category → type-hom-Large-Category C Y X
+    is-iso-hom-Large-Category → hom-Large-Category C Y X
   hom-inv-is-iso-hom-Large-Category =
     hom-inv-is-iso-hom-Large-Precategory
       ( large-precategory-Large-Category C)
@@ -91,7 +91,7 @@ module _
   (f : iso-Large-Category C X Y)
   where
 
-  hom-iso-Large-Category : type-hom-Large-Category C X Y
+  hom-iso-Large-Category : hom-Large-Category C X Y
   hom-iso-Large-Category =
     hom-iso-Large-Precategory (large-precategory-Large-Category C) f
 
@@ -100,7 +100,7 @@ module _
   is-iso-hom-iso-Large-Category =
     is-iso-hom-iso-Large-Precategory (large-precategory-Large-Category C) f
 
-  hom-inv-iso-Large-Category : type-hom-Large-Category C Y X
+  hom-inv-iso-Large-Category : hom-Large-Category C Y X
   hom-inv-iso-Large-Category =
     hom-inv-iso-Large-Precategory (large-precategory-Large-Category C) f
 
@@ -195,21 +195,21 @@ module _
   where
 
   all-elements-equal-is-iso-hom-Large-Category :
-    (f : type-hom-Large-Category C X Y)
+    (f : hom-Large-Category C X Y)
     (H K : is-iso-hom-Large-Category C f) → H ＝ K
   all-elements-equal-is-iso-hom-Large-Category =
     all-elements-equal-is-iso-hom-Large-Precategory
       ( large-precategory-Large-Category C)
 
   is-prop-is-iso-hom-Large-Category :
-    (f : type-hom-Large-Category C X Y) →
+    (f : hom-Large-Category C X Y) →
     is-prop (is-iso-hom-Large-Category C f)
   is-prop-is-iso-hom-Large-Category f =
     is-prop-all-elements-equal
       ( all-elements-equal-is-iso-hom-Large-Category f)
 
   is-iso-prop-hom-Large-Category :
-    (f : type-hom-Large-Category C X Y) → Prop (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
+    (f : hom-Large-Category C X Y) → Prop (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
   is-iso-prop-hom-Large-Category =
     is-iso-prop-hom-Large-Precategory (large-precategory-Large-Category C)
 ```
@@ -260,14 +260,14 @@ module _
   {X : obj-Large-Category C l1}
   {Y : obj-Large-Category C l2}
   {Z : obj-Large-Category C l3}
-  {g : type-hom-Large-Category C Y Z}
-  {f : type-hom-Large-Category C X Y}
+  {g : hom-Large-Category C Y Z}
+  {f : hom-Large-Category C X Y}
   where
 
   hom-comp-is-iso-hom-Large-Category :
     is-iso-hom-Large-Category C g →
     is-iso-hom-Large-Category C f →
-    type-hom-Large-Category C Z X
+    hom-Large-Category C Z X
   hom-comp-is-iso-hom-Large-Category =
     hom-comp-is-iso-hom-Large-Precategory (large-precategory-Large-Category C)
 
@@ -315,7 +315,7 @@ module _
   where
 
   hom-comp-iso-Large-Category :
-    type-hom-Large-Category C X Z
+    hom-Large-Category C X Z
   hom-comp-iso-Large-Category =
     hom-comp-iso-Large-Precategory (large-precategory-Large-Category C) g f
 
@@ -333,7 +333,7 @@ module _
     comp-iso-Large-Precategory (large-precategory-Large-Category C) g f
 
   hom-inv-comp-iso-Large-Category :
-    type-hom-Large-Category C Z X
+    hom-Large-Category C Z X
   hom-inv-comp-iso-Large-Category =
     hom-inv-iso-Large-Category C comp-iso-Large-Category
 
@@ -361,7 +361,7 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Category α β) {l1 l2 : Level}
   {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
-  {f : type-hom-Large-Category C X Y}
+  {f : hom-Large-Category C X Y}
   where
 
   is-iso-inv-is-iso-hom-Large-Category :
@@ -504,14 +504,14 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Category α β) {l1 l2 : Level}
   {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
-  {f : type-hom-Large-Category C X Y}
+  {f : hom-Large-Category C X Y}
   (H :
     {l3 : Level} (Z : obj-Large-Category C l3) →
     is-equiv (precomp-hom-Large-Category C f Z))
   where
 
   hom-inv-is-iso-is-equiv-precomp-hom-Large-Category :
-    type-hom-Large-Category C Y X
+    hom-Large-Category C Y X
   hom-inv-is-iso-is-equiv-precomp-hom-Large-Category =
     hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory
       ( large-precategory-Large-Category C)
@@ -579,14 +579,14 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Category α β) {l1 l2 : Level}
   {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2}
-  {f : type-hom-Large-Category C X Y}
+  {f : hom-Large-Category C X Y}
   (H :
     {l3 : Level} (Z : obj-Large-Category C l3) →
     is-equiv (postcomp-hom-Large-Category C Z f))
   where
 
   hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category :
-    type-hom-Large-Category C Y X
+    hom-Large-Category C Y X
   hom-inv-is-iso-is-equiv-postcomp-hom-Large-Category =
     hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory
       ( large-precategory-Large-Category C)
diff --git a/src/category-theory/isomorphisms-in-large-precategories.lagda.md b/src/category-theory/isomorphisms-in-large-precategories.lagda.md
index 92ce8dd147..a30040013b 100644
--- a/src/category-theory/isomorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/isomorphisms-in-large-precategories.lagda.md
@@ -42,18 +42,18 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : 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)
+  (f : hom-Large-Precategory C X Y)
   where
 
   is-iso-hom-Large-Precategory : UU (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
   is-iso-hom-Large-Precategory =
-    Σ ( type-hom-Large-Precategory C Y X)
+    Σ ( hom-Large-Precategory C Y X)
       ( λ g →
         ( comp-hom-Large-Precategory C f g ＝ id-hom-Large-Precategory C) ×
         ( comp-hom-Large-Precategory C g f ＝ id-hom-Large-Precategory C))
 
   hom-inv-is-iso-hom-Large-Precategory :
-    is-iso-hom-Large-Precategory → type-hom-Large-Precategory C Y X
+    is-iso-hom-Large-Precategory → hom-Large-Precategory C Y X
   hom-inv-is-iso-hom-Large-Precategory = pr1
 
   is-section-hom-inv-is-iso-hom-Large-Precategory :
@@ -80,7 +80,7 @@ module _
 
   iso-Large-Precategory : UU (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2)
   iso-Large-Precategory =
-    Σ (type-hom-Large-Precategory C X Y) (is-iso-hom-Large-Precategory C)
+    Σ (hom-Large-Precategory C X Y) (is-iso-hom-Large-Precategory C)
 
 module _
   {α : Level → Level} {β : Level → Level → Level}
@@ -89,14 +89,14 @@ module _
   (f : iso-Large-Precategory C X Y)
   where
 
-  hom-iso-Large-Precategory : type-hom-Large-Precategory C X Y
+  hom-iso-Large-Precategory : hom-Large-Precategory C X Y
   hom-iso-Large-Precategory = pr1 f
 
   is-iso-hom-iso-Large-Precategory :
     is-iso-hom-Large-Precategory C hom-iso-Large-Precategory
   is-iso-hom-iso-Large-Precategory = pr2 f
 
-  hom-inv-iso-Large-Precategory : type-hom-Large-Precategory C Y X
+  hom-inv-iso-Large-Precategory : hom-Large-Precategory C Y X
   hom-inv-iso-Large-Precategory = pr1 (pr2 f)
 
   is-section-hom-inv-iso-Large-Precategory :
@@ -181,18 +181,18 @@ module _
   where
 
   all-elements-equal-is-iso-hom-Large-Precategory :
-    (f : type-hom-Large-Precategory C X Y)
+    (f : hom-Large-Precategory C X Y)
     (H K : is-iso-hom-Large-Precategory C f) → H ＝ K
   all-elements-equal-is-iso-hom-Large-Precategory f (g , p , q) (g' , p' , q') =
     eq-type-subtype
       ( λ g →
         prod-Prop
           ( Id-Prop
-            ( hom-Large-Precategory C Y Y)
+            ( hom-set-Large-Precategory C Y Y)
             ( comp-hom-Large-Precategory C f g)
             ( id-hom-Large-Precategory C))
           ( Id-Prop
-            ( hom-Large-Precategory C X X)
+            ( hom-set-Large-Precategory C X X)
             ( comp-hom-Large-Precategory C g f)
             ( id-hom-Large-Precategory C)))
       ( ( inv (right-unit-law-comp-hom-Large-Precategory C g)) ∙
@@ -202,14 +202,14 @@ module _
         ( left-unit-law-comp-hom-Large-Precategory C g'))
 
   is-prop-is-iso-hom-Large-Precategory :
-    (f : type-hom-Large-Precategory C X Y) →
+    (f : hom-Large-Precategory C X Y) →
     is-prop (is-iso-hom-Large-Precategory C f)
   is-prop-is-iso-hom-Large-Precategory f =
     is-prop-all-elements-equal
       ( all-elements-equal-is-iso-hom-Large-Precategory f)
 
   is-iso-prop-hom-Large-Precategory :
-    (f : type-hom-Large-Precategory C X Y) → Prop (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
+    (f : hom-Large-Precategory C X Y) → Prop (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2)
   pr1 (is-iso-prop-hom-Large-Precategory f) =
     is-iso-hom-Large-Precategory C f
   pr2 (is-iso-prop-hom-Large-Precategory f) =
@@ -248,7 +248,7 @@ module _
   is-set-iso-Large-Precategory =
     is-set-type-subtype
       ( is-iso-prop-hom-Large-Precategory C)
-      ( is-set-type-hom-Large-Precategory C X Y)
+      ( is-set-hom-Large-Precategory C X Y)
 
   iso-set-Large-Precategory : Set (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2)
   pr1 iso-set-Large-Precategory = iso-Large-Precategory C X Y
@@ -264,14 +264,14 @@ module _
   {X : obj-Large-Precategory C l1}
   {Y : obj-Large-Precategory C l2}
   {Z : obj-Large-Precategory C l3}
-  {g : type-hom-Large-Precategory C Y Z}
-  {f : type-hom-Large-Precategory C X Y}
+  {g : hom-Large-Precategory C Y Z}
+  {f : hom-Large-Precategory C X Y}
   where
 
   hom-comp-is-iso-hom-Large-Precategory :
     is-iso-hom-Large-Precategory C g →
     is-iso-hom-Large-Precategory C f →
-    type-hom-Large-Precategory C Z X
+    hom-Large-Precategory C Z X
   hom-comp-is-iso-hom-Large-Precategory q p =
     comp-hom-Large-Precategory C
       ( hom-inv-is-iso-hom-Large-Precategory C f p)
@@ -351,7 +351,7 @@ module _
   where
 
   hom-comp-iso-Large-Precategory :
-    type-hom-Large-Precategory C X Z
+    hom-Large-Precategory C X Z
   hom-comp-iso-Large-Precategory =
     comp-hom-Large-Precategory C
       ( hom-iso-Large-Precategory C g)
@@ -370,7 +370,7 @@ module _
   pr2 comp-iso-Large-Precategory = is-iso-comp-iso-Large-Precategory
 
   hom-inv-comp-iso-Large-Precategory :
-    type-hom-Large-Precategory C Z X
+    hom-Large-Precategory C Z X
   hom-inv-comp-iso-Large-Precategory =
     hom-inv-iso-Large-Precategory C comp-iso-Large-Precategory
 
@@ -398,7 +398,7 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : 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}
+  {f : hom-Large-Precategory C X Y}
   where
 
   is-iso-inv-is-iso-hom-Large-Precategory :
@@ -548,14 +548,14 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : 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}
+  {f : hom-Large-Precategory C X Y}
   (H :
     {l3 : Level} (Z : obj-Large-Precategory C l3) →
     is-equiv (precomp-hom-Large-Precategory C f Z))
   where
 
   hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory :
-    type-hom-Large-Precategory C Y X
+    hom-Large-Precategory C Y X
   hom-inv-is-iso-is-equiv-precomp-hom-Large-Precategory =
     map-inv-is-equiv (H X) (id-hom-Large-Precategory C)
 
@@ -629,14 +629,14 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : 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}
+  {f : hom-Large-Precategory C X Y}
   (H :
     {l3 : Level} (Z : obj-Large-Precategory C l3) →
     is-equiv (postcomp-hom-Large-Precategory C Z f))
   where
 
   hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory :
-    type-hom-Large-Precategory C Y X
+    hom-Large-Precategory C Y X
   hom-inv-is-iso-is-equiv-postcomp-hom-Large-Precategory =
     map-inv-is-equiv (H Y) (id-hom-Large-Precategory C)
 
diff --git a/src/category-theory/isomorphisms-in-precategories.lagda.md b/src/category-theory/isomorphisms-in-precategories.lagda.md
index 973f79f69b..cf6d9c14b0 100644
--- a/src/category-theory/isomorphisms-in-precategories.lagda.md
+++ b/src/category-theory/isomorphisms-in-precategories.lagda.md
@@ -40,10 +40,10 @@ is-iso-hom-Precategory :
   {l1 l2 : Level}
   (C : Precategory l1 l2)
   {x y : obj-Precategory C}
-  (f : type-hom-Precategory C x y) →
+  (f : hom-Precategory C x y) →
   UU l2
 is-iso-hom-Precategory C {x} {y} f =
-  Σ ( type-hom-Precategory C y x)
+  Σ ( hom-Precategory C y x)
     ( λ g →
       ( comp-hom-Precategory C f g ＝ id-hom-Precategory C) ×
       ( comp-hom-Precategory C g f ＝ id-hom-Precategory C))
@@ -52,11 +52,11 @@ module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
   {x y : obj-Precategory C}
-  {f : type-hom-Precategory C x y}
+  {f : hom-Precategory C x y}
   where
 
   hom-inv-is-iso-hom-Precategory :
-    is-iso-hom-Precategory C f → type-hom-Precategory C y x
+    is-iso-hom-Precategory C f → hom-Precategory C y x
   hom-inv-is-iso-hom-Precategory = pr1
 
   is-section-hom-inv-is-iso-hom-Precategory :
@@ -82,7 +82,7 @@ module _
   where
 
   iso-Precategory : UU l2
-  iso-Precategory = Σ (type-hom-Precategory C x y) (is-iso-hom-Precategory C)
+  iso-Precategory = Σ (hom-Precategory C x y) (is-iso-hom-Precategory C)
 
 module _
   {l1 l2 : Level}
@@ -91,14 +91,14 @@ module _
   (f : iso-Precategory C x y)
   where
 
-  hom-iso-Precategory : type-hom-Precategory C x y
+  hom-iso-Precategory : hom-Precategory C x y
   hom-iso-Precategory = pr1 f
 
   is-iso-hom-iso-Precategory :
     is-iso-hom-Precategory C hom-iso-Precategory
   is-iso-hom-iso-Precategory = pr2 f
 
-  hom-inv-iso-Precategory : type-hom-Precategory C y x
+  hom-inv-iso-Precategory : hom-Precategory C y x
   hom-inv-iso-Precategory =
     hom-inv-is-iso-hom-Precategory C
       ( is-iso-hom-iso-Precategory)
@@ -183,7 +183,7 @@ module _
   where
 
   all-elements-equal-is-iso-hom-Precategory :
-    (f : type-hom-Precategory C x y)
+    (f : hom-Precategory C x y)
     (H K : is-iso-hom-Precategory C f) → H ＝ K
   all-elements-equal-is-iso-hom-Precategory f
     (g , p , q) (g' , p' , q') =
@@ -191,11 +191,11 @@ module _
       ( λ g →
         prod-Prop
           ( Id-Prop
-            ( hom-Precategory C y y)
+            ( hom-set-Precategory C y y)
             ( comp-hom-Precategory C f g)
             ( id-hom-Precategory C))
           ( Id-Prop
-            ( hom-Precategory C x x)
+            ( hom-set-Precategory C x x)
             ( comp-hom-Precategory C g f)
             ( id-hom-Precategory C)))
       ( ( inv (right-unit-law-comp-hom-Precategory C g)) ∙
@@ -205,14 +205,14 @@ module _
         ( left-unit-law-comp-hom-Precategory C g'))
 
   is-prop-is-iso-hom-Precategory :
-    (f : type-hom-Precategory C x y) →
+    (f : hom-Precategory C x y) →
     is-prop (is-iso-hom-Precategory C f)
   is-prop-is-iso-hom-Precategory f =
     is-prop-all-elements-equal
       ( all-elements-equal-is-iso-hom-Precategory f)
 
   is-iso-prop-hom-Precategory :
-    (f : type-hom-Precategory C x y) → Prop l2
+    (f : hom-Precategory C x y) → Prop l2
   pr1 (is-iso-prop-hom-Precategory f) = is-iso-hom-Precategory C f
   pr2 (is-iso-prop-hom-Precategory f) = is-prop-is-iso-hom-Precategory f
 ```
@@ -250,7 +250,7 @@ module _
   is-set-iso-Precategory =
     is-set-type-subtype
       ( is-iso-prop-hom-Precategory C)
-      ( is-set-type-hom-Precategory C x y)
+      ( is-set-hom-Precategory C x y)
 
   iso-set-Precategory : Set l2
   pr1 iso-set-Precategory = iso-Precategory C x y
@@ -264,14 +264,14 @@ module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
   {x y z : obj-Precategory C}
-  {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}
   where
 
   hom-comp-is-iso-hom-Precategory :
     is-iso-hom-Precategory C g →
     is-iso-hom-Precategory C f →
-    type-hom-Precategory C z x
+    hom-Precategory C z x
   hom-comp-is-iso-hom-Precategory q p =
     comp-hom-Precategory C
       ( hom-inv-is-iso-hom-Precategory C p)
@@ -350,7 +350,7 @@ module _
   where
 
   hom-comp-iso-Precategory :
-    type-hom-Precategory C x z
+    hom-Precategory C x z
   hom-comp-iso-Precategory =
     comp-hom-Precategory C
       ( hom-iso-Precategory C g)
@@ -367,7 +367,7 @@ module _
   pr1 comp-iso-Precategory = hom-comp-iso-Precategory
   pr2 comp-iso-Precategory = is-iso-comp-iso-Precategory
 
-  hom-inv-comp-iso-Precategory : type-hom-Precategory C z x
+  hom-inv-comp-iso-Precategory : hom-Precategory C z x
   hom-inv-comp-iso-Precategory =
     hom-inv-iso-Precategory C comp-iso-Precategory
 
@@ -395,7 +395,7 @@ module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
   {x y : obj-Precategory C}
-  {f : type-hom-Precategory C x y}
+  {f : hom-Precategory C x y}
   where
 
   is-iso-inv-is-iso-hom-Precategory :
@@ -543,11 +543,11 @@ module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
   {x y : obj-Precategory C}
-  {f : type-hom-Precategory C x y}
+  {f : hom-Precategory C x y}
   (H : (z : obj-Precategory C) → is-equiv (precomp-hom-Precategory C f z))
   where
 
-  hom-inv-is-iso-is-equiv-precomp-hom-Precategory : type-hom-Precategory C y x
+  hom-inv-is-iso-is-equiv-precomp-hom-Precategory : hom-Precategory C y x
   hom-inv-is-iso-is-equiv-precomp-hom-Precategory =
     map-inv-is-equiv (H x) (id-hom-Precategory C)
 
@@ -620,11 +620,11 @@ module _
   {l1 l2 : Level}
   (C : Precategory l1 l2)
   {x y : obj-Precategory C}
-  {f : type-hom-Precategory C x y}
+  {f : hom-Precategory C x y}
   (H : (z : obj-Precategory C) → is-equiv (postcomp-hom-Precategory C f z))
   where
 
-  hom-inv-is-iso-is-equiv-postcomp-hom-Precategory : type-hom-Precategory C y x
+  hom-inv-is-iso-is-equiv-postcomp-hom-Precategory : hom-Precategory C y x
   hom-inv-is-iso-is-equiv-postcomp-hom-Precategory =
     map-inv-is-equiv (H y) (id-hom-Precategory C)
 
@@ -677,11 +677,11 @@ module _
   where
 
   is-prop-iso-Precategory :
-    is-prop (type-hom-Precategory C x y) → is-prop (iso-Precategory C x y)
+    is-prop (hom-Precategory C x y) → is-prop (iso-Precategory C x y)
   is-prop-iso-Precategory = is-prop-type-subtype (is-iso-prop-hom-Precategory C)
 
   iso-prop-Precategory :
-    is-prop (type-hom-Precategory C x y) → Prop l2
+    is-prop (hom-Precategory C x y) → Prop l2
   pr1 (iso-prop-Precategory _) = iso-Precategory C x y
   pr2 (iso-prop-Precategory is-prop-hom-C-x-y) =
     is-prop-iso-Precategory is-prop-hom-C-x-y
@@ -696,10 +696,10 @@ module _
   where
 
   is-iso-is-prop-hom-Precategory' :
-    is-prop (type-hom-Precategory C x x) →
-    is-prop (type-hom-Precategory C y y) →
-    (f : type-hom-Precategory C x y) →
-    type-hom-Precategory C y x →
+    is-prop (hom-Precategory C x x) →
+    is-prop (hom-Precategory C y y) →
+    (f : hom-Precategory C x y) →
+    hom-Precategory C y x →
     is-iso-hom-Precategory C f
   pr1 (is-iso-is-prop-hom-Precategory' _ _ f g) = g
   pr1 (pr2 (is-iso-is-prop-hom-Precategory' _ is-prop-hom-C-y-y f g)) =
@@ -708,26 +708,26 @@ module _
     eq-is-prop is-prop-hom-C-x-x
 
   iso-is-prop-hom-Precategory' :
-    is-prop (type-hom-Precategory C x x) →
-    is-prop (type-hom-Precategory C y y) →
-    type-hom-Precategory C x y →
-    type-hom-Precategory C y x →
+    is-prop (hom-Precategory C x x) →
+    is-prop (hom-Precategory C y y) →
+    hom-Precategory C x y →
+    hom-Precategory C y x →
     iso-Precategory C x y
   pr1 (iso-is-prop-hom-Precategory' _ _ f g) = f
   pr2 (iso-is-prop-hom-Precategory' is-prop-hom-C-x-x is-prop-hom-C-y-y f g) =
     is-iso-is-prop-hom-Precategory' is-prop-hom-C-x-x is-prop-hom-C-y-y f g
 
   is-iso-is-prop-hom-Precategory :
-    ((x' y' : obj-Precategory C) → is-prop (type-hom-Precategory C x' y')) →
-    (f : type-hom-Precategory C x y) → type-hom-Precategory C y x →
+    ((x' y' : obj-Precategory C) → is-prop (hom-Precategory C x' y')) →
+    (f : hom-Precategory C x y) → hom-Precategory C y x →
     is-iso-hom-Precategory C f
   is-iso-is-prop-hom-Precategory is-prop-hom-C =
     is-iso-is-prop-hom-Precategory' (is-prop-hom-C x x) (is-prop-hom-C y y)
 
   iso-is-prop-hom-Precategory :
-    ((x' y' : obj-Precategory C) → is-prop (type-hom-Precategory C x' y')) →
-    type-hom-Precategory C x y →
-    type-hom-Precategory C y x →
+    ((x' y' : obj-Precategory C) → is-prop (hom-Precategory C x' y')) →
+    hom-Precategory C x y →
+    hom-Precategory C y x →
     iso-Precategory C x y
   iso-is-prop-hom-Precategory is-prop-hom-C =
     iso-is-prop-hom-Precategory' (is-prop-hom-C x x) (is-prop-hom-C y y)
diff --git a/src/category-theory/large-categories.lagda.md b/src/category-theory/large-categories.lagda.md
index 3483fa1907..d9cc55ac5e 100644
--- a/src/category-theory/large-categories.lagda.md
+++ b/src/category-theory/large-categories.lagda.md
@@ -67,43 +67,43 @@ module _
   obj-Large-Category =
     obj-Large-Precategory (large-precategory-Large-Category C)
 
-  hom-Large-Category :
+  hom-set-Large-Category :
     {l1 l2 : Level} →
     obj-Large-Category l1 →
     obj-Large-Category l2 →
     Set (β l1 l2)
-  hom-Large-Category =
-    hom-Large-Precategory (large-precategory-Large-Category C)
+  hom-set-Large-Category =
+    hom-set-Large-Precategory (large-precategory-Large-Category C)
 
-  type-hom-Large-Category :
+  hom-Large-Category :
     {l1 l2 : Level}
     (X : obj-Large-Category l1)
     (Y : obj-Large-Category l2) →
     UU (β l1 l2)
-  type-hom-Large-Category X Y = type-Set (hom-Large-Category X Y)
+  hom-Large-Category X Y = type-Set (hom-set-Large-Category X Y)
 
-  is-set-type-hom-Large-Category :
+  is-set-hom-Large-Category :
     {l1 l2 : Level}
     (X : obj-Large-Category l1)
     (Y : obj-Large-Category l2) →
-    is-set (type-hom-Large-Category X Y)
-  is-set-type-hom-Large-Category X Y =
-    is-set-type-Set (hom-Large-Category X Y)
+    is-set (hom-Large-Category X Y)
+  is-set-hom-Large-Category X Y =
+    is-set-type-Set (hom-set-Large-Category X Y)
 
   comp-hom-Large-Category :
     {l1 l2 l3 : Level}
     {X : obj-Large-Category l1}
     {Y : obj-Large-Category l2}
     {Z : obj-Large-Category l3} →
-    type-hom-Large-Category Y Z →
-    type-hom-Large-Category X Y →
-    type-hom-Large-Category X Z
+    hom-Large-Category Y Z →
+    hom-Large-Category X Y →
+    hom-Large-Category X Z
   comp-hom-Large-Category =
     comp-hom-Large-Precategory (large-precategory-Large-Category C)
 
   id-hom-Large-Category :
     {l1 : Level} {X : obj-Large-Category l1} →
-    type-hom-Large-Category X X
+    hom-Large-Category X X
   id-hom-Large-Category =
     id-hom-Large-Precategory (large-precategory-Large-Category C)
 
@@ -113,9 +113,9 @@ module _
     {Y : obj-Large-Category l2}
     {Z : obj-Large-Category l3}
     {W : obj-Large-Category l4} →
-    (h : type-hom-Large-Category Z W)
-    (g : type-hom-Large-Category Y Z)
-    (f : type-hom-Large-Category X Y) →
+    (h : hom-Large-Category Z W)
+    (g : hom-Large-Category Y Z)
+    (f : hom-Large-Category X Y) →
     ( comp-hom-Large-Category (comp-hom-Large-Category h g) f) ＝
     ( comp-hom-Large-Category h (comp-hom-Large-Category g f))
   associative-comp-hom-Large-Category =
@@ -125,7 +125,7 @@ module _
     {l1 l2 : Level}
     {X : obj-Large-Category l1}
     {Y : obj-Large-Category l2}
-    (f : type-hom-Large-Category X Y) →
+    (f : hom-Large-Category X Y) →
     ( comp-hom-Large-Category id-hom-Large-Category f) ＝ f
   left-unit-law-comp-hom-Large-Category =
     left-unit-law-comp-hom-Large-Precategory
@@ -135,7 +135,7 @@ module _
     {l1 l2 : Level}
     {X : obj-Large-Category l1}
     {Y : obj-Large-Category l2}
-    (f : type-hom-Large-Category X Y) →
+    (f : hom-Large-Category X Y) →
     ( comp-hom-Large-Category f id-hom-Large-Category) ＝ f
   right-unit-law-comp-hom-Large-Category =
     right-unit-law-comp-hom-Large-Precategory
@@ -146,8 +146,8 @@ module _
     {X : obj-Large-Category l1}
     {Y : obj-Large-Category l2}
     {Z : obj-Large-Category l3}
-    {g g' : type-hom-Large-Category Y Z} (p : g ＝ g')
-    {f f' : type-hom-Large-Category X Y} (q : f ＝ f') →
+    {g g' : hom-Large-Category Y Z} (p : g ＝ g')
+    {f f' : hom-Large-Category X Y} (q : f ＝ f') →
     comp-hom-Large-Category g f ＝ comp-hom-Large-Category g' f'
   ap-comp-hom-Large-Category p q =
     ap-binary comp-hom-Large-Category p q
@@ -157,18 +157,18 @@ module _
     {X : obj-Large-Category l1}
     {Y : obj-Large-Category l2}
     {Z : obj-Large-Category l3} →
-    type-hom-Large-Category X Y →
-    type-hom-Large-Category Y Z →
-    type-hom-Large-Category X Z
+    hom-Large-Category X Y →
+    hom-Large-Category Y Z →
+    hom-Large-Category X Z
   comp-hom-Large-Category' f g = comp-hom-Large-Category g f
 
   precomp-hom-Large-Category :
     {l1 l2 l3 : Level}
     {X : obj-Large-Category l1}
     {Y : obj-Large-Category l2}
-    (f : type-hom-Large-Category X Y) →
+    (f : hom-Large-Category X Y) →
     (Z : obj-Large-Category l3) →
-    type-hom-Large-Category Y Z → type-hom-Large-Category X Z
+    hom-Large-Category Y Z → hom-Large-Category X Z
   precomp-hom-Large-Category f Z g =
     comp-hom-Large-Category g f
 
@@ -177,8 +177,8 @@ module _
     (X : obj-Large-Category l1)
     {Y : obj-Large-Category l2}
     {Z : obj-Large-Category l3}
-    (f : type-hom-Large-Category Y Z) →
-    type-hom-Large-Category X Y → type-hom-Large-Category X Z
+    (f : hom-Large-Category Y Z) →
+    hom-Large-Category X Y → hom-Large-Category X Z
   postcomp-hom-Large-Category X f g =
     comp-hom-Large-Category f g
 ```
diff --git a/src/category-theory/large-precategories.lagda.md b/src/category-theory/large-precategories.lagda.md
index 120ae06290..f64d4ca310 100644
--- a/src/category-theory/large-precategories.lagda.md
+++ b/src/category-theory/large-precategories.lagda.md
@@ -36,7 +36,7 @@ record
     obj-Large-Precategory :
       (l : Level) → UU (α l)
 
-    hom-Large-Precategory :
+    hom-set-Large-Precategory :
       {l1 l2 : Level} →
       obj-Large-Precategory l1 →
       obj-Large-Precategory l2 →
@@ -47,14 +47,14 @@ record
       {X : obj-Large-Precategory l1}
       {Y : obj-Large-Precategory l2}
       {Z : obj-Large-Precategory l3} →
-      type-Set (hom-Large-Precategory Y Z) →
-      type-Set (hom-Large-Precategory X Y) →
-      type-Set (hom-Large-Precategory X Z)
+      type-Set (hom-set-Large-Precategory Y Z) →
+      type-Set (hom-set-Large-Precategory X Y) →
+      type-Set (hom-set-Large-Precategory X Z)
 
     id-hom-Large-Precategory :
       {l1 : Level}
       {X : obj-Large-Precategory l1} →
-      type-Set (hom-Large-Precategory X X)
+      type-Set (hom-set-Large-Precategory X X)
 
     associative-comp-hom-Large-Precategory :
       {l1 l2 l3 l4 : Level}
@@ -62,9 +62,9 @@ record
       {Y : obj-Large-Precategory l2}
       {Z : obj-Large-Precategory l3}
       {W : obj-Large-Precategory l4} →
-      (h : type-Set (hom-Large-Precategory Z W))
-      (g : type-Set (hom-Large-Precategory Y Z))
-      (f : type-Set (hom-Large-Precategory X Y)) →
+      (h : type-Set (hom-set-Large-Precategory Z W))
+      (g : type-Set (hom-set-Large-Precategory Y Z))
+      (f : type-Set (hom-set-Large-Precategory X Y)) →
       ( comp-hom-Large-Precategory (comp-hom-Large-Precategory h g) f) ＝
       ( comp-hom-Large-Precategory h (comp-hom-Large-Precategory g f))
 
@@ -72,14 +72,14 @@ record
       {l1 l2 : Level}
       {X : obj-Large-Precategory l1}
       {Y : obj-Large-Precategory l2}
-      (f : type-Set (hom-Large-Precategory X Y)) →
+      (f : type-Set (hom-set-Large-Precategory X Y)) →
       ( comp-hom-Large-Precategory id-hom-Large-Precategory f) ＝ f
 
     right-unit-law-comp-hom-Large-Precategory :
       {l1 l2 : Level}
       {X : obj-Large-Precategory l1}
       {Y : obj-Large-Precategory l2}
-      (f : type-Set (hom-Large-Precategory X Y)) →
+      (f : type-Set (hom-set-Large-Precategory X Y)) →
       ( comp-hom-Large-Precategory f id-hom-Large-Precategory) ＝ f
 
 open Large-Precategory public
@@ -92,28 +92,28 @@ module _
   (C : Large-Precategory α β)
   where
 
-  type-hom-Large-Precategory :
+  hom-Large-Precategory :
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory C l2) →
     UU (β l1 l2)
-  type-hom-Large-Precategory X Y = type-Set (hom-Large-Precategory C X Y)
+  hom-Large-Precategory X Y = type-Set (hom-set-Large-Precategory C X Y)
 
-  is-set-type-hom-Large-Precategory :
+  is-set-hom-Large-Precategory :
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1)
     (Y : obj-Large-Precategory C l2) →
-    is-set (type-hom-Large-Precategory X Y)
-  is-set-type-hom-Large-Precategory X Y =
-    is-set-type-Set (hom-Large-Precategory C X Y)
+    is-set (hom-Large-Precategory X Y)
+  is-set-hom-Large-Precategory X Y =
+    is-set-type-Set (hom-set-Large-Precategory C X Y)
 
   ap-comp-hom-Large-Precategory :
     {l1 l2 l3 : Level}
     {X : obj-Large-Precategory C l1}
     {Y : obj-Large-Precategory C l2}
     {Z : obj-Large-Precategory C l3}
-    {g g' : type-hom-Large-Precategory Y Z} (p : g ＝ g')
-    {f f' : type-hom-Large-Precategory X Y} (q : f ＝ f') →
+    {g g' : hom-Large-Precategory Y Z} (p : g ＝ g')
+    {f f' : hom-Large-Precategory X Y} (q : f ＝ f') →
     comp-hom-Large-Precategory C g f ＝
     comp-hom-Large-Precategory C g' f'
   ap-comp-hom-Large-Precategory = ap-binary (comp-hom-Large-Precategory C)
@@ -123,9 +123,9 @@ module _
     {X : obj-Large-Precategory C l1}
     {Y : obj-Large-Precategory C l2}
     {Z : obj-Large-Precategory C l3} →
-    type-hom-Large-Precategory X Y →
-    type-hom-Large-Precategory Y Z →
-    type-hom-Large-Precategory X Z
+    hom-Large-Precategory X Y →
+    hom-Large-Precategory Y Z →
+    hom-Large-Precategory X Z
   comp-hom-Large-Precategory' f g = comp-hom-Large-Precategory C g f
 ```
 
@@ -136,9 +136,9 @@ module _
     {l1 l2 l3 : Level}
     {X : obj-Large-Precategory C l1}
     {Y : obj-Large-Precategory C l2}
-    (f : type-hom-Large-Precategory X Y) →
+    (f : hom-Large-Precategory X Y) →
     (Z : obj-Large-Precategory C l3) →
-    type-hom-Large-Precategory Y Z → type-hom-Large-Precategory X Z
+    hom-Large-Precategory Y Z → hom-Large-Precategory X Z
   precomp-hom-Large-Precategory f Z g =
     comp-hom-Large-Precategory C g f
 ```
@@ -151,8 +151,8 @@ module _
     (X : obj-Large-Precategory C l1)
     {Y : obj-Large-Precategory C l2}
     {Z : obj-Large-Precategory C l3}
-    (f : type-hom-Large-Precategory Y Z) →
-    type-hom-Large-Precategory X Y → type-hom-Large-Precategory X Z
+    (f : hom-Large-Precategory Y Z) →
+    hom-Large-Precategory X Y → hom-Large-Precategory X Z
   postcomp-hom-Large-Precategory X f g =
     comp-hom-Large-Precategory C f g
 ```
@@ -170,7 +170,7 @@ module _
   pr1 (precategory-Large-Precategory l) =
     obj-Large-Precategory C l
   pr1 (pr2 (precategory-Large-Precategory l)) =
-    hom-Large-Precategory C
+    hom-set-Large-Precategory C
   pr1 (pr1 (pr2 (pr2 (precategory-Large-Precategory l)))) =
     comp-hom-Large-Precategory C
   pr2 (pr1 (pr2 (pr2 (precategory-Large-Precategory l)))) =
diff --git a/src/category-theory/maps-precategories.lagda.md b/src/category-theory/maps-precategories.lagda.md
index ffe47fc51f..dcea46aee2 100644
--- a/src/category-theory/maps-precategories.lagda.md
+++ b/src/category-theory/maps-precategories.lagda.md
@@ -10,14 +10,14 @@ module category-theory.maps-precategories where
 open import category-theory.precategories
 
 open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
 open import foundation.cartesian-product-types
-open import foundation.functoriality-dependent-pair-types
-open import foundation.function-extensionality
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
+open import foundation.function-extensionality
 open import foundation.function-types
-open import foundation.binary-relations
+open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopies
 open import foundation.homotopy-induction
@@ -55,8 +55,8 @@ module _
     Σ ( obj-Precategory C → obj-Precategory D)
       ( λ F₀ →
         {x y : obj-Precategory C} →
-        type-hom-Precategory C x y →
-        type-hom-Precategory D (F₀ x) (F₀ y))
+        hom-Precategory C x y →
+        hom-Precategory D (F₀ x) (F₀ y))
 
   map-obj-map-Precategory :
     (F : map-Precategory) → obj-Precategory C → obj-Precategory D
@@ -65,8 +65,8 @@ module _
   map-hom-map-Precategory :
     (F : map-Precategory)
     {x y : obj-Precategory C} →
-    type-hom-Precategory C x y →
-    type-hom-Precategory D
+    hom-Precategory C x y →
+    hom-Precategory D
       ( map-obj-map-Precategory F x)
       ( map-obj-map-Precategory F y)
   map-hom-map-Precategory = pr2
diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
index 043c3a13b4..268d2b540e 100644
--- a/src/category-theory/monomorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
@@ -34,7 +34,7 @@ module _
   {α : Level → Level} {β : Level → Level → Level}
   (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
   (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
-  (f : type-hom-Large-Precategory C X Y)
+  (f : hom-Large-Precategory C X Y)
   where
 
   is-mono-Large-Precategory-Prop : Prop (α l3 ⊔ β l3 l1 ⊔ β l3 l2)
@@ -92,12 +92,12 @@ module _
                     ( left-unit-law-comp-hom-Large-Precategory C h)))))))
       ( λ p →
         eq-is-prop
-          ( is-set-type-hom-Large-Precategory C Z Y
+          ( is-set-hom-Large-Precategory C Z Y
             ( comp-hom-Large-Precategory C
               ( hom-iso-Large-Precategory C f)
               ( g))
             ( comp-hom-Large-Precategory C
               ( hom-iso-Large-Precategory C f)
               ( h))))
-      ( λ p → eq-is-prop (is-set-type-hom-Large-Precategory C Z X g h))
+      ( λ p → eq-is-prop (is-set-hom-Large-Precategory C Z X g h))
 ```
diff --git a/src/category-theory/natural-isomorphisms-large-precategories.lagda.md b/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
index dfc4b200ac..76a586f5f9 100644
--- a/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-large-precategories.lagda.md
@@ -57,7 +57,7 @@ module _
         { l1 l2 : Level}
         { X : obj-Large-Precategory C l1}
         { Y : obj-Large-Precategory C l2}
-        ( f : type-hom-Large-Precategory C X Y) →
+        ( f : hom-Large-Precategory C X Y) →
         coherence-square-Large-Precategory D
           ( hom-iso-Large-Precategory D
             ( components-natural-isomorphism-Large-Precategory X))
diff --git a/src/category-theory/natural-numbers-object-precategories.lagda.md b/src/category-theory/natural-numbers-object-precategories.lagda.md
index 86a94bb668..b55eb9b842 100644
--- a/src/category-theory/natural-numbers-object-precategories.lagda.md
+++ b/src/category-theory/natural-numbers-object-precategories.lagda.md
@@ -38,13 +38,13 @@ module _
 
   is-natural-numbers-object-Precategory :
     (n : obj-Precategory C) →
-    type-hom-Precategory C t n → type-hom-Precategory C n n → UU (l1 ⊔ l2)
+    hom-Precategory C t n → hom-Precategory C n n → UU (l1 ⊔ l2)
   is-natural-numbers-object-Precategory n z s =
     (x : obj-Precategory C)
-    (q : type-hom-Precategory C t x)
-    (f : type-hom-Precategory C x x) →
+    (q : hom-Precategory C t x)
+    (f : hom-Precategory C x x) →
     ∃!
-      ( type-hom-Precategory C n x)
+      ( hom-Precategory C n x)
       ( λ u →
         ( comp-hom-Precategory C u z ＝ q) ×
         ( comp-hom-Precategory C u s ＝ comp-hom-Precategory C f u))
@@ -52,8 +52,8 @@ module _
   natural-numbers-object-Precategory : UU (l1 ⊔ l2)
   natural-numbers-object-Precategory =
     Σ (obj-Precategory C) λ n →
-    Σ (type-hom-Precategory C t n) λ z →
-    Σ (type-hom-Precategory C n n) λ s →
+    Σ (hom-Precategory C t n) λ z →
+    Σ (hom-Precategory C n n) λ s →
       is-natural-numbers-object-Precategory n z s
 
 module _
@@ -66,23 +66,23 @@ module _
   object-natural-numbers-object-Precategory = pr1 nno
 
   zero-natural-numbers-object-Precategory :
-    type-hom-Precategory C t object-natural-numbers-object-Precategory
+    hom-Precategory C t object-natural-numbers-object-Precategory
   zero-natural-numbers-object-Precategory = pr1 (pr2 nno)
 
   succ-natural-numbers-object-Precategory :
-    type-hom-Precategory C
+    hom-Precategory C
       ( object-natural-numbers-object-Precategory)
       ( object-natural-numbers-object-Precategory)
   succ-natural-numbers-object-Precategory = pr1 (pr2 (pr2 nno))
 
   module _
     (x : obj-Precategory C)
-    (q : type-hom-Precategory C t x)
-    (f : type-hom-Precategory C x x)
+    (q : hom-Precategory C t x)
+    (f : hom-Precategory C x x)
     where
 
     morphism-natural-numbers-object-Precategory :
-      type-hom-Precategory C object-natural-numbers-object-Precategory x
+      hom-Precategory C object-natural-numbers-object-Precategory x
     morphism-natural-numbers-object-Precategory =
       pr1 (pr1 (pr2 (pr2 (pr2 nno)) x q f))
 
@@ -103,7 +103,7 @@ module _
 
     is-unique-morphism-natural-numbers-object-Precategory :
       ( u' :
-        type-hom-Precategory C object-natural-numbers-object-Precategory x) →
+        hom-Precategory C object-natural-numbers-object-Precategory x) →
       comp-hom-Precategory C u' zero-natural-numbers-object-Precategory ＝ q →
       comp-hom-Precategory C u' succ-natural-numbers-object-Precategory ＝
       comp-hom-Precategory C f u' →
diff --git a/src/category-theory/natural-transformations-large-precategories.lagda.md b/src/category-theory/natural-transformations-large-precategories.lagda.md
index f7e32919f5..9c03cd7e84 100644
--- a/src/category-theory/natural-transformations-large-precategories.lagda.md
+++ b/src/category-theory/natural-transformations-large-precategories.lagda.md
@@ -41,10 +41,10 @@ coherence-square-Large-Precategory :
   {B : obj-Large-Precategory C l2}
   {X : obj-Large-Precategory C l3}
   {Y : obj-Large-Precategory C l4}
-  (top : type-hom-Large-Precategory C A B)
-  (left : type-hom-Large-Precategory C A X)
-  (right : type-hom-Large-Precategory C B Y)
-  (bottom : type-hom-Large-Precategory C X Y) →
+  (top : hom-Large-Precategory C A B)
+  (left : hom-Large-Precategory C A X)
+  (right : hom-Large-Precategory C B Y)
+  (bottom : hom-Large-Precategory C X Y) →
   UU (βC l1 l4)
 coherence-square-Large-Precategory C top left right bottom =
   comp-hom-Large-Precategory C right top ＝
@@ -62,7 +62,7 @@ module _
   hom-family-functor-Large-Precategory : UUω
   hom-family-functor-Large-Precategory =
     {l : Level} (X : obj-Large-Precategory C l) →
-    type-hom-Large-Precategory D
+    hom-Large-Precategory D
       ( map-obj-functor-Large-Precategory F X)
       ( map-obj-functor-Large-Precategory G X)
 
@@ -75,7 +75,7 @@ module _
       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) →
+        (f : hom-Large-Precategory C X Y) →
         coherence-square-Large-Precategory D
           ( hom-family-natural-transformation-Large-Precategory X)
           ( 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
index b10480f3b6..5fbaa5e894 100644
--- a/src/category-theory/natural-transformations-precategories.lagda.md
+++ b/src/category-theory/natural-transformations-precategories.lagda.md
@@ -50,14 +50,14 @@ module _
   hom-family-functor-Precategory : UU (l1 ⊔ l4)
   hom-family-functor-Precategory =
     (x : obj-Precategory C) →
-    type-hom-Precategory D
+    hom-Precategory D
       ( map-obj-functor-Precategory C D F x)
       ( map-obj-functor-Precategory C D G x)
 
   is-natural-transformation-Precategory :
     hom-family-functor-Precategory → UU (l1 ⊔ l2 ⊔ l4)
   is-natural-transformation-Precategory γ =
-    {x y : obj-Precategory C} (f : type-hom-Precategory C x y) →
+    {x y : obj-Precategory C} (f : hom-Precategory C x y) →
     ( comp-hom-Precategory D (map-hom-functor-Precategory C D G f) (γ x)) ＝
     ( comp-hom-Precategory D (γ y) (map-hom-functor-Precategory C D F f))
 
@@ -155,7 +155,7 @@ module _
           ( λ y →
             is-prop-Π
               ( λ f →
-                is-set-type-hom-Precategory D
+                is-set-hom-Precategory D
                   ( map-obj-functor-Precategory C D F x)
                   ( map-obj-functor-Precategory C D G y)
                   ( comp-hom-Precategory D
@@ -201,7 +201,7 @@ module _
     is-set-Σ
       ( is-set-Π
         ( λ x →
-          is-set-type-hom-Precategory D
+          is-set-hom-Precategory D
             ( map-obj-functor-Precategory C D F x)
             ( map-obj-functor-Precategory C D G x)))
       ( λ α →
diff --git a/src/category-theory/one-object-precategories.lagda.md b/src/category-theory/one-object-precategories.lagda.md
index 768c46d211..94483f34cb 100644
--- a/src/category-theory/one-object-precategories.lagda.md
+++ b/src/category-theory/one-object-precategories.lagda.md
@@ -61,28 +61,28 @@ module _
   {l : Level} (M : Monoid l)
   where
 
-  hom-one-object-precategory-Monoid :
+  hom-set-one-object-precategory-Monoid :
     unit → unit → Set l
-  hom-one-object-precategory-Monoid star star = set-Monoid M
+  hom-set-one-object-precategory-Monoid star star = set-Monoid M
 
-  type-hom-one-object-precategory-Monoid :
+  hom-one-object-precategory-Monoid :
     unit → unit → UU l
-  type-hom-one-object-precategory-Monoid x y =
-    type-Set (hom-one-object-precategory-Monoid x y)
+  hom-one-object-precategory-Monoid x y =
+    type-Set (hom-set-one-object-precategory-Monoid x y)
 
   comp-hom-one-object-precategory-Monoid :
     {x y z : unit} →
-    type-hom-one-object-precategory-Monoid y z →
-    type-hom-one-object-precategory-Monoid x y →
-    type-hom-one-object-precategory-Monoid x z
+    hom-one-object-precategory-Monoid y z →
+    hom-one-object-precategory-Monoid x y →
+    hom-one-object-precategory-Monoid x z
   comp-hom-one-object-precategory-Monoid {star} {star} {star} =
     mul-Monoid M
 
   associative-comp-hom-one-object-precategory-Monoid :
     {x y z w : unit} →
-    (h : type-hom-one-object-precategory-Monoid z w)
-    (g : type-hom-one-object-precategory-Monoid y z)
-    (f : type-hom-one-object-precategory-Monoid x y) →
+    (h : hom-one-object-precategory-Monoid z w)
+    (g : hom-one-object-precategory-Monoid y z)
+    (f : hom-one-object-precategory-Monoid x y) →
     comp-hom-one-object-precategory-Monoid
       ( comp-hom-one-object-precategory-Monoid h g)
       ( f) ＝
@@ -95,18 +95,18 @@ module _
 
   associative-composition-structure-one-object-precategory-Monoid :
     associative-composition-structure-Set
-      hom-one-object-precategory-Monoid
+      hom-set-one-object-precategory-Monoid
   pr1 associative-composition-structure-one-object-precategory-Monoid =
     comp-hom-one-object-precategory-Monoid
   pr2 associative-composition-structure-one-object-precategory-Monoid =
     associative-comp-hom-one-object-precategory-Monoid
 
   id-hom-one-object-precategory-Monoid :
-    (x : unit) → type-hom-one-object-precategory-Monoid x x
+    (x : unit) → hom-one-object-precategory-Monoid x x
   id-hom-one-object-precategory-Monoid star = unit-Monoid M
 
   left-unit-law-comp-hom-one-object-precategory-Monoid :
-    {x y : unit} (f : type-hom-one-object-precategory-Monoid x y) →
+    {x y : unit} (f : hom-one-object-precategory-Monoid x y) →
     comp-hom-one-object-precategory-Monoid
       ( id-hom-one-object-precategory-Monoid y)
       ( f) ＝
@@ -115,7 +115,7 @@ module _
     left-unit-law-mul-Monoid M
 
   right-unit-law-comp-hom-one-object-precategory-Monoid :
-    {x y : unit} (f : type-hom-one-object-precategory-Monoid x y) →
+    {x y : unit} (f : hom-one-object-precategory-Monoid x y) →
     comp-hom-one-object-precategory-Monoid
       ( f)
       ( id-hom-one-object-precategory-Monoid x) ＝
@@ -125,7 +125,7 @@ module _
 
   is-unital-composition-structure-one-object-precategory-Monoid :
     is-unital-composition-structure-Set
-      hom-one-object-precategory-Monoid
+      hom-set-one-object-precategory-Monoid
       associative-composition-structure-one-object-precategory-Monoid
   pr1 is-unital-composition-structure-one-object-precategory-Monoid =
     id-hom-one-object-precategory-Monoid
@@ -137,7 +137,7 @@ module _
   precategory-one-object-precategory-Monoid : Precategory lzero l
   pr1 precategory-one-object-precategory-Monoid = unit
   pr1 (pr2 precategory-one-object-precategory-Monoid) =
-    hom-one-object-precategory-Monoid
+    hom-set-one-object-precategory-Monoid
   pr1 (pr2 (pr2 precategory-one-object-precategory-Monoid)) =
     associative-composition-structure-one-object-precategory-Monoid
   pr2 (pr2 (pr2 precategory-one-object-precategory-Monoid)) =
diff --git a/src/category-theory/opposite-precategories.lagda.md b/src/category-theory/opposite-precategories.lagda.md
index ca4c62b9bc..a6b4bcf8ce 100644
--- a/src/category-theory/opposite-precategories.lagda.md
+++ b/src/category-theory/opposite-precategories.lagda.md
@@ -30,7 +30,7 @@ module _
 
   opposite-Precategory : Precategory l1 l2
   pr1 opposite-Precategory = obj-Precategory C
-  pr1 (pr2 opposite-Precategory) x y = hom-Precategory C y x
+  pr1 (pr2 opposite-Precategory) x y = hom-set-Precategory C y x
   pr1 (pr1 (pr2 (pr2 opposite-Precategory))) f g = comp-hom-Precategory C g f
   pr2 (pr1 (pr2 (pr2 opposite-Precategory))) f g h =
     inv (associative-comp-hom-Precategory C h g f)
diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md
index fc3e3af816..9b36644117 100644
--- a/src/category-theory/precategories.lagda.md
+++ b/src/category-theory/precategories.lagda.md
@@ -77,39 +77,39 @@ module _
   obj-Precategory : UU l1
   obj-Precategory = pr1 C
 
-  hom-Precategory : (x y : obj-Precategory) → Set l2
-  hom-Precategory = pr1 (pr2 C)
+  hom-set-Precategory : (x y : obj-Precategory) → Set l2
+  hom-set-Precategory = pr1 (pr2 C)
 
-  type-hom-Precategory : (x y : obj-Precategory) → UU l2
-  type-hom-Precategory x y = type-Set (hom-Precategory x y)
+  hom-Precategory : (x y : obj-Precategory) → UU l2
+  hom-Precategory x y = type-Set (hom-set-Precategory x y)
 
-  is-set-type-hom-Precategory :
-    (x y : obj-Precategory) → is-set (type-hom-Precategory x y)
-  is-set-type-hom-Precategory x y = is-set-type-Set (hom-Precategory x y)
+  is-set-hom-Precategory :
+    (x y : obj-Precategory) → is-set (hom-Precategory x y)
+  is-set-hom-Precategory x y = is-set-type-Set (hom-set-Precategory x y)
 
   associative-composition-structure-Precategory :
-    associative-composition-structure-Set hom-Precategory
+    associative-composition-structure-Set hom-set-Precategory
   associative-composition-structure-Precategory = pr1 (pr2 (pr2 C))
 
   comp-hom-Precategory :
     {x y z : obj-Precategory} →
-    type-hom-Precategory y z →
-    type-hom-Precategory x y →
-    type-hom-Precategory x z
+    hom-Precategory y z →
+    hom-Precategory x y →
+    hom-Precategory x z
   comp-hom-Precategory = pr1 associative-composition-structure-Precategory
 
   comp-hom-Precategory' :
     {x y z : obj-Precategory} →
-    type-hom-Precategory x y →
-    type-hom-Precategory y z →
-    type-hom-Precategory x z
+    hom-Precategory x y →
+    hom-Precategory y z →
+    hom-Precategory x z
   comp-hom-Precategory' f g = comp-hom-Precategory g f
 
   associative-comp-hom-Precategory :
     {x y z w : obj-Precategory}
-    (h : type-hom-Precategory z w)
-    (g : type-hom-Precategory y z)
-    (f : type-hom-Precategory x y) →
+    (h : hom-Precategory z w)
+    (g : hom-Precategory y z)
+    (f : hom-Precategory x y) →
     ( comp-hom-Precategory (comp-hom-Precategory h g) f) ＝
     ( comp-hom-Precategory h (comp-hom-Precategory g f))
   associative-comp-hom-Precategory =
@@ -117,21 +117,21 @@ module _
 
   is-unital-composition-structure-Precategory :
     is-unital-composition-structure-Set
-      hom-Precategory
+      hom-set-Precategory
       associative-composition-structure-Precategory
   is-unital-composition-structure-Precategory = pr2 (pr2 (pr2 C))
 
-  id-hom-Precategory : {x : obj-Precategory} → type-hom-Precategory x x
+  id-hom-Precategory : {x : obj-Precategory} → hom-Precategory x x
   id-hom-Precategory {x} = pr1 is-unital-composition-structure-Precategory x
 
   left-unit-law-comp-hom-Precategory :
-    {x y : obj-Precategory} (f : type-hom-Precategory x y) →
+    {x y : obj-Precategory} (f : hom-Precategory x y) →
     comp-hom-Precategory id-hom-Precategory f ＝ f
   left-unit-law-comp-hom-Precategory =
     pr1 (pr2 is-unital-composition-structure-Precategory)
 
   right-unit-law-comp-hom-Precategory :
-    {x y : obj-Precategory} (f : type-hom-Precategory x y) →
+    {x y : obj-Precategory} (f : hom-Precategory x y) →
     comp-hom-Precategory f id-hom-Precategory ＝ f
   right-unit-law-comp-hom-Precategory =
     pr2 (pr2 is-unital-composition-structure-Precategory)
@@ -142,8 +142,8 @@ module _
 ```agda
 precomp-hom-Precategory :
   {l1 l2 : Level} (C : Precategory l1 l2) {x y : obj-Precategory C}
-  (f : type-hom-Precategory C x y) (z : obj-Precategory C) →
-  type-hom-Precategory C y z → type-hom-Precategory C x z
+  (f : hom-Precategory C x y) (z : obj-Precategory C) →
+  hom-Precategory C y z → hom-Precategory C x z
 precomp-hom-Precategory C f z g = comp-hom-Precategory C g f
 ```
 
@@ -152,8 +152,8 @@ precomp-hom-Precategory C f z g = comp-hom-Precategory C g f
 ```agda
 postcomp-hom-Precategory :
   {l1 l2 : Level} (C : Precategory l1 l2) {x y : obj-Precategory C}
-  (f : type-hom-Precategory C x y) (z : obj-Precategory C) →
-  type-hom-Precategory C z x → type-hom-Precategory C z y
+  (f : hom-Precategory C x y) (z : obj-Precategory C) →
+  hom-Precategory C z x → hom-Precategory C z y
 postcomp-hom-Precategory C f z = comp-hom-Precategory C f
 ```
 
diff --git a/src/category-theory/pregroupoids.lagda.md b/src/category-theory/pregroupoids.lagda.md
index 3bf8406238..d773657520 100644
--- a/src/category-theory/pregroupoids.lagda.md
+++ b/src/category-theory/pregroupoids.lagda.md
@@ -34,7 +34,7 @@ is-groupoid-Precategory-Prop C =
         ( obj-Precategory C)
         ( λ y →
           Π-Prop
-            ( type-hom-Precategory C x y)
+            ( hom-Precategory C x y)
             ( is-iso-prop-hom-Precategory C)))
 
 is-groupoid-Precategory :
diff --git a/src/category-theory/products-in-precategories.lagda.md b/src/category-theory/products-in-precategories.lagda.md
index f20ecd37f2..fa0135533f 100644
--- a/src/category-theory/products-in-precategories.lagda.md
+++ b/src/category-theory/products-in-precategories.lagda.md
@@ -44,21 +44,21 @@ module _
 
   is-product-Precategory :
     (x y p : obj-Precategory C) →
-    type-hom-Precategory C p x →
-    type-hom-Precategory C p y →
+    hom-Precategory C p x →
+    hom-Precategory C p y →
     UU (l1 ⊔ l2)
   is-product-Precategory x y p l r =
     (z : obj-Precategory C)
-    (f : type-hom-Precategory C z x) →
-    (g : type-hom-Precategory C z y) →
-    (∃! (type-hom-Precategory C z p) λ h →
+    (f : hom-Precategory C z x) →
+    (g : hom-Precategory C z y) →
+    (∃! (hom-Precategory C z p) λ h →
         (comp-hom-Precategory C l h ＝ f) × (comp-hom-Precategory C r h ＝ g))
 
   product-Precategory : obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
   product-Precategory x y =
     Σ (obj-Precategory C) λ p →
-    Σ (type-hom-Precategory C p x) λ l →
-    Σ (type-hom-Precategory C p y) λ r →
+    Σ (hom-Precategory C p x) λ l →
+    Σ (hom-Precategory C p y) λ r →
       is-product-Precategory x y p l r
 
   has-all-binary-products-Precategory : UU (l1 ⊔ l2)
@@ -76,22 +76,22 @@ module _
 
   pr1-product-Precategory :
     (x y : obj-Precategory C) →
-    type-hom-Precategory C (object-product-Precategory x y) x
+    hom-Precategory C (object-product-Precategory x y) x
   pr1-product-Precategory x y = pr1 (pr2 (t x y))
 
   pr2-product-Precategory :
     (x y : obj-Precategory C) →
-    type-hom-Precategory C (object-product-Precategory x y) y
+    hom-Precategory C (object-product-Precategory x y) y
   pr2-product-Precategory x y = pr1 (pr2 (pr2 (t x y)))
 
   module _
     (x y z : obj-Precategory C)
-    (f : type-hom-Precategory C z x)
-    (g : type-hom-Precategory C z y)
+    (f : hom-Precategory C z x)
+    (g : hom-Precategory C z y)
     where
 
     morphism-into-product-Precategory :
-      type-hom-Precategory C z (object-product-Precategory x y)
+      hom-Precategory C z (object-product-Precategory x y)
     morphism-into-product-Precategory =
       pr1 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g))
 
@@ -110,7 +110,7 @@ module _
       pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g)))
 
     is-unique-morphism-into-product-Precategory :
-      (h : type-hom-Precategory C z (object-product-Precategory x y)) →
+      (h : hom-Precategory C z (object-product-Precategory x y)) →
       comp-hom-Precategory C (pr1-product-Precategory x y) h ＝ f →
       comp-hom-Precategory C (pr2-product-Precategory x y) h ＝ g →
       morphism-into-product-Precategory ＝ h
@@ -120,8 +120,8 @@ module _
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   (x y p : obj-Precategory C)
-  (l : type-hom-Precategory C p x)
-  (r : type-hom-Precategory C p y)
+  (l : hom-Precategory C p x)
+  (r : hom-Precategory C p y)
   where
 
   is-prop-is-product-Precategory : is-prop (is-product-Precategory C x y p l r)
@@ -149,12 +149,12 @@ module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   (t : has-all-binary-products-Precategory C)
   {x₁ x₂ y₁ y₂ : obj-Precategory C}
-  (f : type-hom-Precategory C x₁ y₁)
-  (g : type-hom-Precategory C x₂ y₂)
+  (f : hom-Precategory C x₁ y₁)
+  (g : hom-Precategory C x₂ y₂)
   where
 
   map-product-Precategory :
-    type-hom-Precategory C
+    hom-Precategory C
       (object-product-Precategory C t x₁ x₂)
       (object-product-Precategory C t y₁ y₂)
   map-product-Precategory =
diff --git a/src/category-theory/products-of-precategories.lagda.md b/src/category-theory/products-of-precategories.lagda.md
index fe0e20e903..7a38191f9a 100644
--- a/src/category-theory/products-of-precategories.lagda.md
+++ b/src/category-theory/products-of-precategories.lagda.md
@@ -39,7 +39,7 @@ module _
     Precategory (l1 ⊔ l3) (l2 ⊔ l4)
   pr1 prod-Precategory = obj-Precategory C × obj-Precategory D
   pr1 (pr2 prod-Precategory) (x , y) (x' , y') =
-    prod-Set (hom-Precategory C x x') (hom-Precategory D y y')
+    prod-Set (hom-set-Precategory C x x') (hom-set-Precategory D y y')
   pr1 (pr1 (pr1 (pr2 (pr2 prod-Precategory))) (f' , g') (f , g)) =
     comp-hom-Precategory C f' f
   pr2 (pr1 (pr1 (pr2 (pr2 prod-Precategory))) (f' , g') (f , g)) =
diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md
index faf2f6890b..a170840a46 100644
--- a/src/category-theory/pullbacks-in-precategories.lagda.md
+++ b/src/category-theory/pullbacks-in-precategories.lagda.md
@@ -46,60 +46,60 @@ module _
 
   is-pullback-Precategory :
     (x y z : obj-Precategory C) →
-    (f : type-hom-Precategory C y x) →
-    (g : type-hom-Precategory C z x) →
+    (f : hom-Precategory C y x) →
+    (g : hom-Precategory C z x) →
     (w : obj-Precategory C) →
-    (p₁ : type-hom-Precategory C w y) →
-    (p₂ : type-hom-Precategory C w z) →
+    (p₁ : hom-Precategory C w y) →
+    (p₂ : hom-Precategory C w z) →
     comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂ →
     UU (l1 ⊔ l2)
   is-pullback-Precategory x y z f g w p₁ p₂ _ =
     (w' : obj-Precategory C) →
-    (p₁' : type-hom-Precategory C w' y) →
-    (p₂' : type-hom-Precategory C w' z) →
+    (p₁' : hom-Precategory C w' y) →
+    (p₂' : hom-Precategory C w' z) →
     comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂' →
     ∃!
-      ( type-hom-Precategory C w' w)
+      ( hom-Precategory C w' w)
       ( λ h →
         ( comp-hom-Precategory C p₁ h ＝ p₁') ×
         ( comp-hom-Precategory C p₂ h ＝ p₂'))
 
   pullback-Precategory :
     (x y z : obj-Precategory C) →
-    type-hom-Precategory C y x →
-    type-hom-Precategory C z x →
+    hom-Precategory C y x →
+    hom-Precategory C z x →
     UU (l1 ⊔ l2)
   pullback-Precategory x y z f g =
     Σ (obj-Precategory C) λ w →
-    Σ (type-hom-Precategory C w y) λ p₁ →
-    Σ (type-hom-Precategory C w z) λ p₂ →
+    Σ (hom-Precategory C w y) λ p₁ →
+    Σ (hom-Precategory C w z) λ p₂ →
     Σ (comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂) λ α →
       is-pullback-Precategory x y z f g w p₁ p₂ α
 
   has-all-pullback-Precategory : UU (l1 ⊔ l2)
   has-all-pullback-Precategory =
     (x y z : obj-Precategory C) →
-    (f : type-hom-Precategory C y x) →
-    (g : type-hom-Precategory C z x) →
+    (f : hom-Precategory C y x) →
+    (g : hom-Precategory C z x) →
     pullback-Precategory x y z f g
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   (t : has-all-pullback-Precategory C)
   (x y z : obj-Precategory C)
-  (f : type-hom-Precategory C y x)
-  (g : type-hom-Precategory C z x)
+  (f : hom-Precategory C y x)
+  (g : hom-Precategory C z x)
   where
 
   object-pullback-Precategory : obj-Precategory C
   object-pullback-Precategory = pr1 (t x y z f g)
 
   pr1-pullback-Precategory :
-    type-hom-Precategory C object-pullback-Precategory y
+    hom-Precategory C object-pullback-Precategory y
   pr1-pullback-Precategory = pr1 (pr2 (t x y z f g))
 
   pr2-pullback-Precategory :
-    type-hom-Precategory C object-pullback-Precategory z
+    hom-Precategory C object-pullback-Precategory z
   pr2-pullback-Precategory = pr1 (pr2 (pr2 (t x y z f g)))
 
   pullback-square-Precategory-comm :
@@ -109,13 +109,13 @@ module _
 
   module _
     (w' : obj-Precategory C)
-    (p₁' : type-hom-Precategory C w' y)
-    (p₂' : type-hom-Precategory C w' z)
+    (p₁' : hom-Precategory C w' y)
+    (p₂' : hom-Precategory C w' z)
     (α : comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂')
     where
 
     morphism-into-pullback-Precategory :
-      type-hom-Precategory C w' object-pullback-Precategory
+      hom-Precategory C w' object-pullback-Precategory
     morphism-into-pullback-Precategory =
       pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))
 
@@ -136,7 +136,7 @@ module _
       pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))
 
     is-unique-morphism-into-pullback-Precategory :
-      (h' : type-hom-Precategory C w' object-pullback-Precategory) →
+      (h' : hom-Precategory C w' object-pullback-Precategory) →
       comp-hom-Precategory C pr1-pullback-Precategory h' ＝ p₁' →
       comp-hom-Precategory C pr2-pullback-Precategory h' ＝ p₂' →
       morphism-into-pullback-Precategory ＝ h'
@@ -148,11 +148,11 @@ module _
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   (x y z : obj-Precategory C)
-  (f : type-hom-Precategory C y x)
-  (g : type-hom-Precategory C z x)
+  (f : hom-Precategory C y x)
+  (g : hom-Precategory C z x)
   (w : obj-Precategory C)
-  (p₁ : type-hom-Precategory C w y)
-  (p₂ : type-hom-Precategory C w z)
+  (p₁ : hom-Precategory C w y)
+  (p₂ : hom-Precategory C w z)
   (α : comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂)
   where
 
diff --git a/src/category-theory/representable-functors-categories.lagda.md b/src/category-theory/representable-functors-categories.lagda.md
index 5ead665ee0..2a0b07f5d5 100644
--- a/src/category-theory/representable-functors-categories.lagda.md
+++ b/src/category-theory/representable-functors-categories.lagda.md
@@ -55,7 +55,7 @@ components `hom c x → hom b x` are defined by precomposition with `f`.
 ```agda
 rep-natural-transformation-Category :
   {l1 l2 : Level} (C : Category l1 l2) (b c : obj-Category C)
-  (f : type-hom-Category C b c) →
+  (f : hom-Category C b c) →
   natural-transformation-Category
     ( C)
     ( Set-Category l2)
diff --git a/src/category-theory/representable-functors-precategories.lagda.md b/src/category-theory/representable-functors-precategories.lagda.md
index 47d507c5d7..dfa5952b64 100644
--- a/src/category-theory/representable-functors-precategories.lagda.md
+++ b/src/category-theory/representable-functors-precategories.lagda.md
@@ -41,7 +41,7 @@ associativity and the left unit law for the precategory `C`.
 representable-functor-Precategory :
   {l1 l2 : Level} (C : Precategory l1 l2) (c : obj-Precategory C) →
   functor-Precategory C (Set-Precategory l2)
-pr1 (representable-functor-Precategory C c) = hom-Precategory C c
+pr1 (representable-functor-Precategory C c) = hom-set-Precategory C c
 pr1 (pr2 (representable-functor-Precategory C c)) g =
   postcomp-hom-Precategory C g c
 pr1 (pr2 (pr2 (representable-functor-Precategory C c))) h g =
@@ -60,7 +60,7 @@ components `hom c x → hom b x` are defined by precomposition with `f`.
 ```agda
 rep-natural-transformation-Precategory :
   {l1 l2 : Level} (C : Precategory l1 l2) (b c : obj-Precategory C)
-  (f : type-hom-Precategory C b c) →
+  (f : hom-Precategory C b c) →
   natural-transformation-Precategory
     ( C)
     ( Set-Precategory l2)
diff --git a/src/category-theory/representing-arrow-category.lagda.md b/src/category-theory/representing-arrow-category.lagda.md
index babfe89641..32ad822db0 100644
--- a/src/category-theory/representing-arrow-category.lagda.md
+++ b/src/category-theory/representing-arrow-category.lagda.md
@@ -49,15 +49,15 @@ implication on the [booleans](foundation.booleans.md).
 obj-representing-arrow : UU lzero
 obj-representing-arrow = bool
 
-hom-representing-arrow :
+hom-set-representing-arrow :
   obj-representing-arrow → obj-representing-arrow → Set lzero
-hom-representing-arrow true true = unit-Set
-hom-representing-arrow true false = empty-Set
-hom-representing-arrow false _ = unit-Set
+hom-set-representing-arrow true true = unit-Set
+hom-set-representing-arrow true false = empty-Set
+hom-set-representing-arrow false _ = unit-Set
 
-type-hom-representing-arrow :
+hom-representing-arrow :
   obj-representing-arrow → obj-representing-arrow → UU lzero
-type-hom-representing-arrow x y = type-Set (hom-representing-arrow x y)
+hom-representing-arrow x y = type-Set (hom-set-representing-arrow x y)
 ```
 
 ### The precategory structure of the representing arrow
@@ -65,51 +65,51 @@ type-hom-representing-arrow x y = type-Set (hom-representing-arrow x y)
 ```agda
 comp-hom-representing-arrow :
   {x y z : obj-representing-arrow} →
-  type-hom-representing-arrow y z →
-  type-hom-representing-arrow x y →
-  type-hom-representing-arrow x z
+  hom-representing-arrow y z →
+  hom-representing-arrow x y →
+  hom-representing-arrow x z
 comp-hom-representing-arrow {true} {true} {true} _ _ = star
 comp-hom-representing-arrow {false} _ _ = star
 
 associative-comp-hom-representing-arrow :
   {x y z w : obj-representing-arrow} →
-  (h : type-hom-representing-arrow z w)
-  (g : type-hom-representing-arrow y z)
-  (f : type-hom-representing-arrow x y) →
+  (h : hom-representing-arrow z w)
+  (g : hom-representing-arrow y z)
+  (f : hom-representing-arrow x y) →
   comp-hom-representing-arrow {x} (comp-hom-representing-arrow {y} h g) f ＝
   comp-hom-representing-arrow {x} h (comp-hom-representing-arrow {x} g f)
 associative-comp-hom-representing-arrow {true} {true} {true} {true} h g f = refl
 associative-comp-hom-representing-arrow {false} h g f = refl
 
 associative-composition-structure-representing-arrow :
-  associative-composition-structure-Set hom-representing-arrow
+  associative-composition-structure-Set hom-set-representing-arrow
 pr1 associative-composition-structure-representing-arrow {x} =
   comp-hom-representing-arrow {x}
 pr2 associative-composition-structure-representing-arrow =
   associative-comp-hom-representing-arrow
 
 id-hom-representing-arrow :
-  {x : obj-representing-arrow} → type-hom-representing-arrow x x
+  {x : obj-representing-arrow} → hom-representing-arrow x x
 id-hom-representing-arrow {true} = star
 id-hom-representing-arrow {false} = star
 
 left-unit-law-comp-hom-representing-arrow :
   {x y : obj-representing-arrow} →
-  (f : type-hom-representing-arrow x y) →
+  (f : hom-representing-arrow x y) →
   comp-hom-representing-arrow {x} (id-hom-representing-arrow {y}) f ＝ f
 left-unit-law-comp-hom-representing-arrow {true} {true} f = refl
 left-unit-law-comp-hom-representing-arrow {false} f = refl
 
 right-unit-law-comp-hom-representing-arrow :
   {x y : obj-representing-arrow} →
-  (f : type-hom-representing-arrow x y) →
+  (f : hom-representing-arrow x y) →
   comp-hom-representing-arrow {x} f (id-hom-representing-arrow {x}) ＝ f
 right-unit-law-comp-hom-representing-arrow {true} {true} f = refl
 right-unit-law-comp-hom-representing-arrow {false} f = refl
 
 is-unital-composition-structure-representing-arrow :
   is-unital-composition-structure-Set
-    ( hom-representing-arrow)
+    ( hom-set-representing-arrow)
     ( associative-composition-structure-representing-arrow)
 pr1 is-unital-composition-structure-representing-arrow x =
   id-hom-representing-arrow {x}
@@ -120,7 +120,7 @@ pr2 (pr2 is-unital-composition-structure-representing-arrow) =
 
 representing-arrow-Precategory : Precategory lzero lzero
 pr1 representing-arrow-Precategory = obj-representing-arrow
-pr1 (pr2 representing-arrow-Precategory) = hom-representing-arrow
+pr1 (pr2 representing-arrow-Precategory) = hom-set-representing-arrow
 pr1 (pr2 (pr2 representing-arrow-Precategory)) =
   associative-composition-structure-representing-arrow
 pr2 (pr2 (pr2 representing-arrow-Precategory)) =
diff --git a/src/category-theory/sieves-in-categories.lagda.md b/src/category-theory/sieves-in-categories.lagda.md
index fbf6f43982..b03c38c8e2 100644
--- a/src/category-theory/sieves-in-categories.lagda.md
+++ b/src/category-theory/sieves-in-categories.lagda.md
@@ -37,7 +37,7 @@ module _
   is-sieve-Category-Prop :
     { l3 : Level}
     ( S : (X Y : obj-Category C) →
-    subtype l3 (type-hom-Category C X Y)) → Prop (l1 ⊔ l2 ⊔ l3)
+    subtype l3 (hom-Category C X Y)) → Prop (l1 ⊔ l2 ⊔ l3)
   is-sieve-Category-Prop S =
     Π-Prop
       ( obj-Category C)
@@ -52,7 +52,7 @@ module _
                   ( type-subtype (S Y X))
                   ( λ f →
                     Π-Prop
-                      ( type-hom-Category C Z Y)
+                      ( hom-Category C Z Y)
                       ( λ g →
                         S Z X
                           ( comp-hom-Category
@@ -61,12 +61,12 @@ module _
   is-sieve-Category :
     { l3 : Level}
     ( S : (X Y : obj-Category C) →
-    subtype l3 (type-hom-Category C X Y)) → UU (l1 ⊔ l2 ⊔ l3)
+    subtype l3 (hom-Category C X Y)) → UU (l1 ⊔ l2 ⊔ l3)
   is-sieve-Category S = type-Prop (is-sieve-Category-Prop S)
 
   is-prop-is-sieve-Category :
     { l3 : Level}
-    ( S : (X Y : obj-Category C) → subtype l3 (type-hom-Category C X Y)) →
+    ( S : (X Y : obj-Category C) → subtype l3 (hom-Category C X Y)) →
     is-prop (is-sieve-Category S)
   is-prop-is-sieve-Category S = is-prop-type-Prop (is-sieve-Category-Prop S)
 ```
diff --git a/src/category-theory/slice-precategories.lagda.md b/src/category-theory/slice-precategories.lagda.md
index c30c46ded4..bda00ed05f 100644
--- a/src/category-theory/slice-precategories.lagda.md
+++ b/src/category-theory/slice-precategories.lagda.md
@@ -46,48 +46,49 @@ module _
 
   obj-Slice-Precategory : UU (l1 ⊔ l2)
   obj-Slice-Precategory =
-    Σ (obj-Precategory C) (λ A → type-hom-Precategory C A X)
+    Σ (obj-Precategory C) (λ A → hom-Precategory C A X)
 
-  hom-Slice-Precategory : obj-Slice-Precategory → obj-Slice-Precategory → Set l2
-  hom-Slice-Precategory (A , f) (B , g) =
+  hom-set-Slice-Precategory :
+    obj-Slice-Precategory → obj-Slice-Precategory → Set l2
+  hom-set-Slice-Precategory (A , f) (B , g) =
     Σ-Set
-      ( hom-Precategory C A B)
+      ( hom-set-Precategory C A B)
       ( λ h →
         set-Prop
-          ( Id-Prop (hom-Precategory C A X) f (comp-hom-Precategory C g h)))
+          ( Id-Prop (hom-set-Precategory C A X) f (comp-hom-Precategory C g h)))
 
-  type-hom-Slice-Precategory :
+  hom-Slice-Precategory :
     obj-Slice-Precategory → obj-Slice-Precategory → UU l2
-  type-hom-Slice-Precategory A B = type-Set (hom-Slice-Precategory A B)
+  hom-Slice-Precategory A B = type-Set (hom-set-Slice-Precategory A B)
 
-  is-set-type-hom-Slice-Precategory :
-    (A B : obj-Slice-Precategory) → is-set (type-hom-Slice-Precategory A B)
-  is-set-type-hom-Slice-Precategory A B =
-    is-set-type-Set (hom-Slice-Precategory A B)
+  is-set-hom-Slice-Precategory :
+    (A B : obj-Slice-Precategory) → is-set (hom-Slice-Precategory A B)
+  is-set-hom-Slice-Precategory A B =
+    is-set-type-Set (hom-set-Slice-Precategory A B)
 
   Eq-hom-Slice-Precategory :
     {A B : obj-Slice-Precategory}
-    (f g : type-hom-Slice-Precategory A B) → UU l2
+    (f g : hom-Slice-Precategory A B) → UU l2
   Eq-hom-Slice-Precategory f g = (pr1 f ＝ pr1 g)
 
   refl-Eq-hom-Slice-Precategory :
-    {A B : obj-Slice-Precategory} (f : type-hom-Slice-Precategory A B) →
+    {A B : obj-Slice-Precategory} (f : hom-Slice-Precategory A B) →
     Eq-hom-Slice-Precategory f f
   refl-Eq-hom-Slice-Precategory f = refl
 
   extensionality-hom-Slice-Precategory :
-    {A B : obj-Slice-Precategory} (f g : type-hom-Slice-Precategory A B) →
+    {A B : obj-Slice-Precategory} (f g : hom-Slice-Precategory A B) →
     (f ＝ g) ≃ Eq-hom-Slice-Precategory f g
   extensionality-hom-Slice-Precategory {A} {B} =
     extensionality-type-subtype'
       ( λ h →
         Id-Prop
-          ( hom-Precategory C (pr1 A) X)
+          ( hom-set-Precategory C (pr1 A) X)
           ( pr2 A)
           ( comp-hom-Precategory C (pr2 B) h))
 
   eq-hom-Slice-Precategory :
-    {A B : obj-Slice-Precategory} (f g : type-hom-Slice-Precategory A B) →
+    {A B : obj-Slice-Precategory} (f g : hom-Slice-Precategory A B) →
     Eq-hom-Slice-Precategory f g → f ＝ g
   eq-hom-Slice-Precategory f g =
     map-inv-equiv (extensionality-hom-Slice-Precategory f g)
@@ -97,7 +98,7 @@ module _
 
 ```agda
   id-hom-Slice-Precategory :
-    (A : obj-Slice-Precategory) → type-hom-Slice-Precategory A A
+    (A : obj-Slice-Precategory) → hom-Slice-Precategory A A
   pr1 (id-hom-Slice-Precategory A) = id-hom-Precategory C
   pr2 (id-hom-Slice-Precategory A) =
     inv (right-unit-law-comp-hom-Precategory C (pr2 A))
@@ -108,8 +109,8 @@ module _
 ```agda
   comp-hom-Slice-Precategory :
     {A1 A2 A3 : obj-Slice-Precategory} →
-    type-hom-Slice-Precategory A2 A3 → type-hom-Slice-Precategory A1 A2 →
-    type-hom-Slice-Precategory A1 A3
+    hom-Slice-Precategory A2 A3 → hom-Slice-Precategory A1 A2 →
+    hom-Slice-Precategory A1 A3
   pr1 (comp-hom-Slice-Precategory g f) = comp-hom-Precategory C (pr1 g) (pr1 f)
   pr2 (comp-hom-Slice-Precategory g f) =
     ( pr2 f) ∙
@@ -122,9 +123,9 @@ module _
 ```agda
   associative-comp-hom-Slice-Precategory :
     {A1 A2 A3 A4 : obj-Slice-Precategory} →
-    (h : type-hom-Slice-Precategory A3 A4)
-    (g : type-hom-Slice-Precategory A2 A3)
-    (f : type-hom-Slice-Precategory A1 A2) →
+    (h : hom-Slice-Precategory A3 A4)
+    (g : hom-Slice-Precategory A2 A3)
+    (f : hom-Slice-Precategory A1 A2) →
     ( comp-hom-Slice-Precategory (comp-hom-Slice-Precategory h g) f) ＝
     ( comp-hom-Slice-Precategory h (comp-hom-Slice-Precategory g f))
   associative-comp-hom-Slice-Precategory h g f =
@@ -138,7 +139,7 @@ module _
 
 ```agda
   left-unit-law-comp-hom-Slice-Precategory :
-    {A B : obj-Slice-Precategory} (f : type-hom-Slice-Precategory A B) →
+    {A B : obj-Slice-Precategory} (f : hom-Slice-Precategory A B) →
     comp-hom-Slice-Precategory (id-hom-Slice-Precategory B) f ＝ f
   left-unit-law-comp-hom-Slice-Precategory f =
     eq-hom-Slice-Precategory
@@ -151,7 +152,7 @@ module _
 
 ```agda
   right-unit-law-comp-hom-Slice-Precategory :
-    {A B : obj-Slice-Precategory} (f : type-hom-Slice-Precategory A B) →
+    {A B : obj-Slice-Precategory} (f : hom-Slice-Precategory A B) →
     comp-hom-Slice-Precategory f (id-hom-Slice-Precategory A) ＝ f
   right-unit-law-comp-hom-Slice-Precategory f =
     eq-hom-Slice-Precategory
@@ -165,7 +166,7 @@ module _
 ```agda
   Slice-Precategory : Precategory (l1 ⊔ l2) l2
   pr1 Slice-Precategory = obj-Slice-Precategory
-  pr1 (pr2 Slice-Precategory) = hom-Slice-Precategory
+  pr1 (pr2 Slice-Precategory) = hom-set-Slice-Precategory
   pr1 (pr1 (pr2 (pr2 Slice-Precategory))) = comp-hom-Slice-Precategory
   pr2 (pr1 (pr2 (pr2 Slice-Precategory))) =
     associative-comp-hom-Slice-Precategory
@@ -193,7 +194,7 @@ module _
   pr1 terminal-obj-Precategory-Slice-Precategory = (X , id-hom-Precategory C)
   pr2 terminal-obj-Precategory-Slice-Precategory (A , f) =
     is-contr-equiv
-      ( Σ (type-hom-Precategory C A X) (λ g → f ＝ g))
+      ( Σ (hom-Precategory C A X) (λ g → f ＝ g))
       ( equiv-tot
         ( λ g → equiv-concat' f (left-unit-law-comp-hom-Precategory C g)))
       ( is-contr-total-path f)
@@ -204,13 +205,13 @@ module _
 ```agda
 module _
   {l1 l2 : Level} (C : Precategory l1 l2) {A X Y : obj-Precategory C}
-  (f : type-hom-Precategory C X A) (g : type-hom-Precategory C Y A)
+  (f : hom-Precategory C X A) (g : hom-Precategory C Y A)
   where
 
   module _
     {W : obj-Precategory C}
-    (p₁ : type-hom-Precategory C W X) (p₂ : type-hom-Precategory C W Y)
-    (p : type-hom-Precategory C W A)
+    (p₁ : hom-Precategory C W X) (p₂ : hom-Precategory C W Y)
+    (p : hom-Precategory C W A)
     (α₁ : p ＝ comp-hom-Precategory C f p₁)
     (α₂ : p ＝ comp-hom-Precategory C g p₂)
     (α : comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂)
@@ -225,7 +226,7 @@ module _
       is-contr-Σ-is-prop c d q σ
       where
       c :
-        type-hom-Precategory
+        hom-Precategory
           ( Slice-Precategory C A)
           ( Z , comp-hom-Precategory C f h₁)
           ( W , p)
@@ -258,8 +259,8 @@ module _
               (Slice-Precategory C A) (p₂ , α₂) k ＝ (h₂ , β₂)))
       q k =
         is-prop-prod
-          ( is-set-type-Set (hom-Slice-Precategory C A _ _) _ _)
-          ( is-set-type-Set (hom-Slice-Precategory C A _ _) _ _)
+          ( is-set-type-Set (hom-set-Slice-Precategory C A _ _) _ _)
+          ( is-set-type-Set (hom-set-Slice-Precategory C A _ _) _ _)
 
       σ :
         ∀ k →
@@ -285,7 +286,7 @@ module _
     map-inv-is-pullback-is-product-Slice-Precategory ψ W' p₁' p₂' α' =
       is-contr-Σ-is-prop k γ q σ
       where
-      k : type-hom-Precategory C W' W
+      k : hom-Precategory C W' W
       k =
         pr1
           ( pr1
@@ -324,11 +325,11 @@ module _
           ( comp-hom-Precategory C p₂ k' ＝ p₂'))
       q k' =
         is-prop-prod
-          ( is-set-type-Set (hom-Precategory C _ _) _ _)
-          ( is-set-type-Set (hom-Precategory C _ _) _ _)
+          ( is-set-type-Set (hom-set-Precategory C _ _) _ _)
+          ( is-set-type-Set (hom-set-Precategory C _ _) _ _)
 
       σ :
-        ( k' : type-hom-Precategory C W' W) →
+        ( k' : hom-Precategory C W' W) →
         ( γ' :
           ( comp-hom-Precategory C p₁ k' ＝ p₁') ×
           ( comp-hom-Precategory C p₂ k' ＝ p₂')) →
diff --git a/src/category-theory/terminal-objects-precategories.lagda.md b/src/category-theory/terminal-objects-precategories.lagda.md
index 6e4d638bea..22d9b360c7 100644
--- a/src/category-theory/terminal-objects-precategories.lagda.md
+++ b/src/category-theory/terminal-objects-precategories.lagda.md
@@ -34,7 +34,7 @@ object.
 is-terminal-obj-Precategory :
   {l1 l2 : Level} (C : Precategory l1 l2) → obj-Precategory C → UU (l1 ⊔ l2)
 is-terminal-obj-Precategory C x =
-  (y : obj-Precategory C) → is-contr (type-hom-Precategory C y x)
+  (y : obj-Precategory C) → is-contr (hom-Precategory C y x)
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
@@ -44,12 +44,12 @@ module _
 
   hom-is-terminal-obj-Precategory :
     (y : obj-Precategory C) →
-    type-hom-Precategory C y x
+    hom-Precategory C y x
   hom-is-terminal-obj-Precategory = center ∘ t
 
   is-unique-hom-is-terminal-obj-Precategory :
     (y : obj-Precategory C) →
-    (f : type-hom-Precategory C y x) →
+    (f : hom-Precategory C y x) →
     hom-is-terminal-obj-Precategory y ＝ f
   is-unique-hom-is-terminal-obj-Precategory = contraction ∘ t
 ```
@@ -77,7 +77,7 @@ module _
 
   hom-terminal-obj-Precategory :
     (y : obj-Precategory C) →
-    type-hom-Precategory C y obj-terminal-obj-Precategory
+    hom-Precategory C y obj-terminal-obj-Precategory
   hom-terminal-obj-Precategory =
     hom-is-terminal-obj-Precategory C
       ( obj-terminal-obj-Precategory)
@@ -85,7 +85,7 @@ module _
 
   is-unique-hom-terminal-obj-Precategory :
     (y : obj-Precategory C) →
-    (f : type-hom-Precategory C y obj-terminal-obj-Precategory) →
+    (f : hom-Precategory C y obj-terminal-obj-Precategory) →
     hom-terminal-obj-Precategory y ＝ f
   is-unique-hom-terminal-obj-Precategory =
     is-unique-hom-is-terminal-obj-Precategory C
diff --git a/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md b/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md
index 4a0e88a29e..35d86daf5b 100644
--- a/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md
+++ b/src/commutative-algebra/groups-of-units-commutative-rings.lagda.md
@@ -311,10 +311,10 @@ group-of-units-commutative-ring-functor-Large-Precategory :
     ( Commutative-Ring-Large-Precategory)
     ( Ab-Large-Precategory)
     ( id)
-obj-functor-Large-Precategory
+map-obj-functor-Large-Precategory
   group-of-units-commutative-ring-functor-Large-Precategory =
   abelian-group-of-units-Commutative-Ring
-hom-functor-Large-Precategory
+map-hom-functor-Large-Precategory
   group-of-units-commutative-ring-functor-Large-Precategory {X = A} {Y = B} =
   hom-group-of-units-hom-Commutative-Ring A B
 preserves-comp-functor-Large-Precategory
diff --git a/src/commutative-algebra/homomorphisms-commutative-rings.lagda.md b/src/commutative-algebra/homomorphisms-commutative-rings.lagda.md
index f61e521010..3201fe380c 100644
--- a/src/commutative-algebra/homomorphisms-commutative-rings.lagda.md
+++ b/src/commutative-algebra/homomorphisms-commutative-rings.lagda.md
@@ -69,9 +69,9 @@ module _
   {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2)
   where
 
-  hom-Commutative-Ring : Set (l1 ⊔ l2)
-  hom-Commutative-Ring =
-    hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B)
+  hom-set-Commutative-Ring : Set (l1 ⊔ l2)
+  hom-set-Commutative-Ring =
+    hom-set-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B)
 
   type-hom-Commutative-Ring : UU (l1 ⊔ l2)
   type-hom-Commutative-Ring =
diff --git a/src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md b/src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md
index 60139afbfd..57ad242a0b 100644
--- a/src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md
+++ b/src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md
@@ -36,9 +36,9 @@ module _
   {l1 l2 : Level} (A : Commutative-Semiring l1) (B : Commutative-Semiring l2)
   where
 
-  hom-Commutative-Semiring : Set (l1 ⊔ l2)
-  hom-Commutative-Semiring =
-    hom-Semiring
+  hom-set-Commutative-Semiring : Set (l1 ⊔ l2)
+  hom-set-Commutative-Semiring =
+    hom-set-Semiring
       ( semiring-Commutative-Semiring A)
       ( semiring-Commutative-Semiring B)
 
diff --git a/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md b/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md
index 78b25c085f..974e3b3e61 100644
--- a/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md
+++ b/src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md
@@ -180,7 +180,7 @@ module _
   preserves-order-ideal-radical-ideal-Commutative-Ring I J H = H
 
   ideal-radical-ideal-hom-large-poset-Commutative-Ring :
-    hom-Large-Poset id
+    hom-set-Large-Poset id
       ( radical-ideal-Commutative-Ring-Large-Poset A)
       ( ideal-Commutative-Ring-Large-Poset A)
   map-hom-Large-Preorder
diff --git a/src/commutative-algebra/precategory-of-commutative-rings.lagda.md b/src/commutative-algebra/precategory-of-commutative-rings.lagda.md
index b95d978e93..f7e1024b3b 100644
--- a/src/commutative-algebra/precategory-of-commutative-rings.lagda.md
+++ b/src/commutative-algebra/precategory-of-commutative-rings.lagda.md
@@ -32,9 +32,9 @@ Commutative-Ring-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Commutative-Ring-Large-Precategory =
   Commutative-Ring
-hom-Large-Precategory
+hom-set-Large-Precategory
   Commutative-Ring-Large-Precategory =
-  hom-Commutative-Ring
+  hom-set-Commutative-Ring
 comp-hom-Large-Precategory
   Commutative-Ring-Large-Precategory {X = A} {B} {C} =
   comp-hom-Commutative-Ring A B C
diff --git a/src/commutative-algebra/precategory-of-commutative-semirings.lagda.md b/src/commutative-algebra/precategory-of-commutative-semirings.lagda.md
index 6c944c5a7d..a8e99a50cf 100644
--- a/src/commutative-algebra/precategory-of-commutative-semirings.lagda.md
+++ b/src/commutative-algebra/precategory-of-commutative-semirings.lagda.md
@@ -32,9 +32,9 @@ Commutative-Semiring-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Commutative-Semiring-Large-Precategory =
   Commutative-Semiring
-hom-Large-Precategory
+hom-set-Large-Precategory
   Commutative-Semiring-Large-Precategory =
-  hom-Commutative-Semiring
+  hom-set-Commutative-Semiring
 comp-hom-Large-Precategory
   Commutative-Semiring-Large-Precategory {X = A} {B} {C} =
   comp-hom-Commutative-Semiring A B C
diff --git a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
index c328c9d0af..b954547a45 100644
--- a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
+++ b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md
@@ -238,7 +238,7 @@ module _
         ( H))
 
   radical-of-ideal-hom-large-poset-Commutative-Ring :
-    hom-Large-Poset id
+    hom-set-Large-Poset id
       ( ideal-Commutative-Ring-Large-Poset A)
       ( radical-ideal-Commutative-Ring-Large-Poset A)
   map-hom-Large-Preorder
diff --git a/src/finite-algebra/homomorphisms-commutative-finite-rings.lagda.md b/src/finite-algebra/homomorphisms-commutative-finite-rings.lagda.md
index 4e92d05ad0..95c124def9 100644
--- a/src/finite-algebra/homomorphisms-commutative-finite-rings.lagda.md
+++ b/src/finite-algebra/homomorphisms-commutative-finite-rings.lagda.md
@@ -76,9 +76,9 @@ module _
   {l1 l2 : Level} (A : Commutative-Ring-𝔽 l1) (B : Commutative-Ring-𝔽 l2)
   where
 
-  hom-Commutative-Ring-𝔽 : Set (l1 ⊔ l2)
-  hom-Commutative-Ring-𝔽 =
-    hom-Ring (ring-Commutative-Ring-𝔽 A) (ring-Commutative-Ring-𝔽 B)
+  hom-set-Commutative-Ring-𝔽 : Set (l1 ⊔ l2)
+  hom-set-Commutative-Ring-𝔽 =
+    hom-set-Ring (ring-Commutative-Ring-𝔽 A) (ring-Commutative-Ring-𝔽 B)
 
   type-hom-Commutative-Ring-𝔽 : UU (l1 ⊔ l2)
   type-hom-Commutative-Ring-𝔽 =
diff --git a/src/finite-algebra/homomorphisms-finite-rings.lagda.md b/src/finite-algebra/homomorphisms-finite-rings.lagda.md
index 7af69e025b..dbcfbfdf9b 100644
--- a/src/finite-algebra/homomorphisms-finite-rings.lagda.md
+++ b/src/finite-algebra/homomorphisms-finite-rings.lagda.md
@@ -64,9 +64,9 @@ module _
   {l1 l2 : Level} (A : Ring-𝔽 l1) (B : Ring-𝔽 l2)
   where
 
-  hom-Ring-𝔽 : Set (l1 ⊔ l2)
-  hom-Ring-𝔽 =
-    hom-Ring (ring-Ring-𝔽 A) (ring-Ring-𝔽 B)
+  hom-set-Ring-𝔽 : Set (l1 ⊔ l2)
+  hom-set-Ring-𝔽 =
+    hom-set-Ring (ring-Ring-𝔽 A) (ring-Ring-𝔽 B)
 
   type-hom-Ring-𝔽 : UU (l1 ⊔ l2)
   type-hom-Ring-𝔽 =
diff --git a/src/foundation/category-of-sets.lagda.md b/src/foundation/category-of-sets.lagda.md
index d0fcdcfb9a..34d3b3d72a 100644
--- a/src/foundation/category-of-sets.lagda.md
+++ b/src/foundation/category-of-sets.lagda.md
@@ -39,7 +39,7 @@ sets for each universe level, and there is a large category of sets.
 ```agda
 Set-Large-Precategory : Large-Precategory lsuc (_⊔_)
 obj-Large-Precategory Set-Large-Precategory = Set
-hom-Large-Precategory Set-Large-Precategory = hom-Set
+hom-set-Large-Precategory Set-Large-Precategory = hom-Set
 comp-hom-Large-Precategory Set-Large-Precategory g f = g ∘ f
 id-hom-Large-Precategory Set-Large-Precategory = id
 associative-comp-hom-Large-Precategory Set-Large-Precategory h g f = refl
diff --git a/src/group-theory/addition-homomorphisms-abelian-groups.lagda.md b/src/group-theory/addition-homomorphisms-abelian-groups.lagda.md
index e3f5aaef36..6c7d6674f5 100644
--- a/src/group-theory/addition-homomorphisms-abelian-groups.lagda.md
+++ b/src/group-theory/addition-homomorphisms-abelian-groups.lagda.md
@@ -141,7 +141,7 @@ module _
   where
 
   semigroup-hom-Ab : Semigroup (l1 ⊔ l2)
-  pr1 semigroup-hom-Ab = hom-Ab A B
+  pr1 semigroup-hom-Ab = hom-set-Ab A B
   pr1 (pr2 semigroup-hom-Ab) = add-hom-Ab A B
   pr2 (pr2 semigroup-hom-Ab) = associative-add-hom-Ab A B
 
diff --git a/src/group-theory/cores-monoids.lagda.md b/src/group-theory/cores-monoids.lagda.md
index 18f6ea2acb..cb4cd809b5 100644
--- a/src/group-theory/cores-monoids.lagda.md
+++ b/src/group-theory/cores-monoids.lagda.md
@@ -227,10 +227,10 @@ module _
 ```agda
 core-monoid-functor-Large-Precategory :
   functor-Large-Precategory Monoid-Large-Precategory Group-Large-Precategory id
-obj-functor-Large-Precategory
+map-obj-functor-Large-Precategory
   core-monoid-functor-Large-Precategory =
   core-Monoid
-hom-functor-Large-Precategory
+map-hom-functor-Large-Precategory
   core-monoid-functor-Large-Precategory {X = M} {Y = N} =
   hom-core-hom-Monoid M N
 preserves-comp-functor-Large-Precategory
diff --git a/src/group-theory/epimorphisms-groups.lagda.md b/src/group-theory/epimorphisms-groups.lagda.md
index 1071f4fe92..a37e3f5d66 100644
--- a/src/group-theory/epimorphisms-groups.lagda.md
+++ b/src/group-theory/epimorphisms-groups.lagda.md
@@ -26,7 +26,7 @@ A [group homomorphism](group-theory.homomorphisms-groups.md) `f : G → H` is an
 **epimorphism** if the precomposition function
 
 ```text
-  - ∘ f : hom-Group H K → hom-Group G K
+  - ∘ f : hom-set-Group H K → hom-set-Group G K
 ```
 
 is an [embedding](foundation.embeddings.md) for any
diff --git a/src/group-theory/homomorphisms-abelian-groups.lagda.md b/src/group-theory/homomorphisms-abelian-groups.lagda.md
index 83d772abab..b5d7daf939 100644
--- a/src/group-theory/homomorphisms-abelian-groups.lagda.md
+++ b/src/group-theory/homomorphisms-abelian-groups.lagda.md
@@ -38,8 +38,8 @@ module _
   preserves-add-Ab : (type-Ab A → type-Ab B) → UU (l1 ⊔ l2)
   preserves-add-Ab = preserves-mul-Semigroup (semigroup-Ab A) (semigroup-Ab B)
 
-  hom-Ab : Set (l1 ⊔ l2)
-  hom-Ab = hom-Group (group-Ab A) (group-Ab B)
+  hom-set-Ab : Set (l1 ⊔ l2)
+  hom-set-Ab = hom-set-Group (group-Ab A) (group-Ab B)
 
   type-hom-Ab : UU (l1 ⊔ l2)
   type-hom-Ab = type-hom-Group (group-Ab A) (group-Ab B)
diff --git a/src/group-theory/homomorphisms-commutative-monoids.lagda.md b/src/group-theory/homomorphisms-commutative-monoids.lagda.md
index f15680d9ca..64463ecde6 100644
--- a/src/group-theory/homomorphisms-commutative-monoids.lagda.md
+++ b/src/group-theory/homomorphisms-commutative-monoids.lagda.md
@@ -35,9 +35,9 @@ module _
   {l1 l2 : Level} (M1 : Commutative-Monoid l1) (M2 : Commutative-Monoid l2)
   where
 
-  hom-Commutative-Monoid : Set (l1 ⊔ l2)
-  hom-Commutative-Monoid =
-    hom-Monoid (monoid-Commutative-Monoid M1) (monoid-Commutative-Monoid M2)
+  hom-set-Commutative-Monoid : Set (l1 ⊔ l2)
+  hom-set-Commutative-Monoid =
+    hom-set-Monoid (monoid-Commutative-Monoid M1) (monoid-Commutative-Monoid M2)
 
   type-hom-Commutative-Monoid : UU (l1 ⊔ l2)
   type-hom-Commutative-Monoid =
diff --git a/src/group-theory/homomorphisms-concrete-groups.lagda.md b/src/group-theory/homomorphisms-concrete-groups.lagda.md
index 66cc0b9f9b..bbc3ba7919 100644
--- a/src/group-theory/homomorphisms-concrete-groups.lagda.md
+++ b/src/group-theory/homomorphisms-concrete-groups.lagda.md
@@ -45,9 +45,6 @@ module _
   pr1 hom-set-Concrete-Group = hom-Concrete-Group
   pr2 hom-set-Concrete-Group = is-set-hom-Concrete-Group
 
-  hom-Concrete-Group-Set : Set (l1 ⊔ l2)
-  hom-Concrete-Group-Set = pair hom-Concrete-Group is-set-hom-Concrete-Group
-
   classifying-map-hom-Concrete-Group :
     hom-Concrete-Group →
     classifying-type-Concrete-Group G → classifying-type-Concrete-Group H
diff --git a/src/group-theory/homomorphisms-group-actions.lagda.md b/src/group-theory/homomorphisms-group-actions.lagda.md
index dcae0863c5..259b3bb474 100644
--- a/src/group-theory/homomorphisms-group-actions.lagda.md
+++ b/src/group-theory/homomorphisms-group-actions.lagda.md
@@ -191,9 +191,9 @@ module _
             ( map-hom-Abstract-Group-Action G X Y f x)
             ( map-hom-Abstract-Group-Action G X Y g x)))
 
-  hom-Abstract-Group-Action : Set (l1 ⊔ l2 ⊔ l3)
-  pr1 hom-Abstract-Group-Action = type-hom-Abstract-Group-Action G X Y
-  pr2 hom-Abstract-Group-Action = is-set-type-hom-Abstract-Group-Action
+  hom-set-Abstract-Group-Action : Set (l1 ⊔ l2 ⊔ l3)
+  pr1 hom-set-Abstract-Group-Action = type-hom-Abstract-Group-Action G X Y
+  pr2 hom-set-Abstract-Group-Action = is-set-type-hom-Abstract-Group-Action
 ```
 
 ### Composition is associative
diff --git a/src/group-theory/homomorphisms-groups.lagda.md b/src/group-theory/homomorphisms-groups.lagda.md
index 6fcda8d5ec..73a0af10c3 100644
--- a/src/group-theory/homomorphisms-groups.lagda.md
+++ b/src/group-theory/homomorphisms-groups.lagda.md
@@ -136,9 +136,9 @@ module _
   is-set-type-hom-Group =
     is-set-type-hom-Semigroup (semigroup-Group G) (semigroup-Group H)
 
-  hom-Group : Set (l1 ⊔ l2)
-  pr1 hom-Group = type-hom-Group G H
-  pr2 hom-Group = is-set-type-hom-Group
+  hom-set-Group : Set (l1 ⊔ l2)
+  pr1 hom-set-Group = type-hom-Group G H
+  pr2 hom-set-Group = is-set-type-hom-Group
 ```
 
 ### Associativity of composition of group homomorphisms
diff --git a/src/group-theory/homomorphisms-monoids.lagda.md b/src/group-theory/homomorphisms-monoids.lagda.md
index f42a56e160..794c352ae1 100644
--- a/src/group-theory/homomorphisms-monoids.lagda.md
+++ b/src/group-theory/homomorphisms-monoids.lagda.md
@@ -66,14 +66,14 @@ module _
   is-prop-preserves-unit-hom-Semigroup f =
     is-prop-type-Prop (preserves-unit-hom-semigroup-Prop f)
 
-  hom-Monoid : Set (l1 ⊔ l2)
-  hom-Monoid =
+  hom-set-Monoid : Set (l1 ⊔ l2)
+  hom-set-Monoid =
     set-subset
-      ( hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2))
+      ( hom-set-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2))
       ( preserves-unit-hom-semigroup-Prop)
 
   type-hom-Monoid : UU (l1 ⊔ l2)
-  type-hom-Monoid = type-Set hom-Monoid
+  type-hom-Monoid = type-Set hom-set-Monoid
 
 module _
   {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : type-hom-Monoid M N)
diff --git a/src/group-theory/homomorphisms-semigroups.lagda.md b/src/group-theory/homomorphisms-semigroups.lagda.md
index 11c7b0856d..93a5d9f3f1 100644
--- a/src/group-theory/homomorphisms-semigroups.lagda.md
+++ b/src/group-theory/homomorphisms-semigroups.lagda.md
@@ -157,9 +157,9 @@ module _
             ( map-hom-Semigroup f x)
             ( map-hom-Semigroup g x)))
 
-  hom-Semigroup : Set (l1 ⊔ l2)
-  pr1 hom-Semigroup = type-hom-Semigroup
-  pr2 hom-Semigroup = is-set-type-hom-Semigroup
+  hom-set-Semigroup : Set (l1 ⊔ l2)
+  pr1 hom-set-Semigroup = type-hom-Semigroup
+  pr2 hom-set-Semigroup = is-set-type-hom-Semigroup
 
 preserves-mul-id-Semigroup :
   {l : Level} (G : Semigroup l) → preserves-mul-Semigroup G G id
diff --git a/src/group-theory/isomorphisms-monoids.lagda.md b/src/group-theory/isomorphisms-monoids.lagda.md
index e764ba3b8a..4908991d69 100644
--- a/src/group-theory/isomorphisms-monoids.lagda.md
+++ b/src/group-theory/isomorphisms-monoids.lagda.md
@@ -106,7 +106,7 @@ module _
     (f : iso-Monoid) →
     is-iso-hom-Monoid M N (hom-iso-Monoid f)
   is-iso-iso-Monoid =
-    is-iso-iso-Large-Precategory Monoid-Large-Precategory {X = M} {Y = N}
+    is-iso-hom-iso-Large-Precategory Monoid-Large-Precategory {X = M} {Y = N}
 
   hom-inv-iso-Monoid :
     iso-Monoid → type-hom-Monoid N M
@@ -222,7 +222,6 @@ module _
       ( Monoid-Large-Precategory)
       { X = M}
       { Y = N}
-
   is-iso-prop-hom-Monoid :
     (f : type-hom-Monoid M N) → Prop (l1 ⊔ l2)
   is-iso-prop-hom-Monoid =
@@ -244,7 +243,8 @@ module _
     is-set-iso-Large-Precategory Monoid-Large-Precategory {X = M} {Y = N}
 
   iso-set-Monoid : Set (l1 ⊔ l2)
-  iso-set-Monoid = iso-set-Large-Precategory Monoid-Large-Precategory M N
+  iso-set-Monoid =
+    iso-set-Large-Precategory Monoid-Large-Precategory {X = M} {Y = N}
 ```
 
 ### Isomorphisms are stable by composition
diff --git a/src/group-theory/normal-closures-subgroups.lagda.md b/src/group-theory/normal-closures-subgroups.lagda.md
index a545d8c676..29990ecd76 100644
--- a/src/group-theory/normal-closures-subgroups.lagda.md
+++ b/src/group-theory/normal-closures-subgroups.lagda.md
@@ -236,7 +236,7 @@ module _
         ( u))
 
   normal-closure-subgroup-hom-Large-Poset :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( λ l2 → l1 ⊔ l2)
       ( Subgroup-Large-Poset G)
       ( Normal-Subgroup-Large-Poset G)
diff --git a/src/group-theory/normal-cores-subgroups.lagda.md b/src/group-theory/normal-cores-subgroups.lagda.md
index 90aca9f718..5005868a47 100644
--- a/src/group-theory/normal-cores-subgroups.lagda.md
+++ b/src/group-theory/normal-cores-subgroups.lagda.md
@@ -213,7 +213,7 @@ module _
         ( is-contained-in-subgroup-normal-core-Subgroup G H))
 
   normal-core-subgroup-hom-Large-Poset :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( λ l2 → l1 ⊔ l2)
       ( Subgroup-Large-Poset G)
       ( Normal-Subgroup-Large-Poset G)
diff --git a/src/group-theory/normal-subgroups.lagda.md b/src/group-theory/normal-subgroups.lagda.md
index 39c1293188..b701eb644f 100644
--- a/src/group-theory/normal-subgroups.lagda.md
+++ b/src/group-theory/normal-subgroups.lagda.md
@@ -382,7 +382,9 @@ preserves-order-subgroup-Normal-Subgroup G N M = id
 
 subgroup-normal-subgroup-hom-Large-Poset :
   {l1 : Level} (G : Group l1) →
-  hom-Large-Poset id (Normal-Subgroup-Large-Poset G) (Subgroup-Large-Poset G)
+  hom-set-Large-Poset id
+    ( Normal-Subgroup-Large-Poset G)
+    ( Subgroup-Large-Poset G)
 subgroup-normal-subgroup-hom-Large-Poset G =
   make-hom-Large-Preorder
     ( subgroup-Normal-Subgroup G)
diff --git a/src/group-theory/precategory-of-abelian-groups.lagda.md b/src/group-theory/precategory-of-abelian-groups.lagda.md
index fc5ffd415a..60d38dbcce 100644
--- a/src/group-theory/precategory-of-abelian-groups.lagda.md
+++ b/src/group-theory/precategory-of-abelian-groups.lagda.md
@@ -32,9 +32,9 @@ Ab-Large-Precategory : Large-Precategory lsuc (_⊔_)
 Large-Precategory.obj-Large-Precategory
   Ab-Large-Precategory =
   Ab
-Large-Precategory.hom-Large-Precategory
+Large-Precategory.hom-set-Large-Precategory
   Ab-Large-Precategory =
-  hom-Ab
+  hom-set-Ab
 Large-Precategory.comp-hom-Large-Precategory
   Ab-Large-Precategory {X = A} {B} {C} =
   comp-hom-Ab A B C
diff --git a/src/group-theory/precategory-of-commutative-monoids.lagda.md b/src/group-theory/precategory-of-commutative-monoids.lagda.md
index a5cab0d1ca..19b5610636 100644
--- a/src/group-theory/precategory-of-commutative-monoids.lagda.md
+++ b/src/group-theory/precategory-of-commutative-monoids.lagda.md
@@ -31,9 +31,9 @@ Commutative-Monoid-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Commutative-Monoid-Large-Precategory =
   Commutative-Monoid
-hom-Large-Precategory
+hom-set-Large-Precategory
   Commutative-Monoid-Large-Precategory =
-  hom-Commutative-Monoid
+  hom-set-Commutative-Monoid
 comp-hom-Large-Precategory
   Commutative-Monoid-Large-Precategory {X = K} {L} {M} =
   comp-hom-Commutative-Monoid K L M
diff --git a/src/group-theory/precategory-of-concrete-groups.lagda.md b/src/group-theory/precategory-of-concrete-groups.lagda.md
index 840b77fee7..93140e428f 100644
--- a/src/group-theory/precategory-of-concrete-groups.lagda.md
+++ b/src/group-theory/precategory-of-concrete-groups.lagda.md
@@ -26,7 +26,7 @@ Concrete-Group-Large-Precategory : Large-Precategory lsuc (_⊔_)
 obj-Large-Precategory
   Concrete-Group-Large-Precategory =
   Concrete-Group
-hom-Large-Precategory
+hom-set-Large-Precategory
   Concrete-Group-Large-Precategory =
   hom-set-Concrete-Group
 comp-hom-Large-Precategory
diff --git a/src/group-theory/precategory-of-group-actions.lagda.md b/src/group-theory/precategory-of-group-actions.lagda.md
index 954f515f7a..ebd561b72f 100644
--- a/src/group-theory/precategory-of-group-actions.lagda.md
+++ b/src/group-theory/precategory-of-group-actions.lagda.md
@@ -34,9 +34,9 @@ module _
   obj-Large-Precategory
     Abstract-Group-Action-Large-Precategory =
     Abstract-Group-Action G
-  hom-Large-Precategory
+  hom-set-Large-Precategory
     Abstract-Group-Action-Large-Precategory =
-    hom-Abstract-Group-Action G
+    hom-set-Abstract-Group-Action G
   comp-hom-Large-Precategory
     Abstract-Group-Action-Large-Precategory {X = X} {Y} {Z} =
     comp-hom-Abstract-Group-Action G X Y Z
@@ -64,7 +64,8 @@ module _
   Abstract-Group-Action-Precategory :
     (l2 : Level) → Precategory (l1 ⊔ lsuc l2) (l1 ⊔ l2)
   pr1 (Abstract-Group-Action-Precategory l2) = Abstract-Group-Action G l2
-  pr1 (pr2 (Abstract-Group-Action-Precategory l2)) = hom-Abstract-Group-Action G
+  pr1 (pr2 (Abstract-Group-Action-Precategory l2)) =
+    hom-set-Abstract-Group-Action G
   pr1 (pr1 (pr2 (pr2 (Abstract-Group-Action-Precategory l2)))) {X} {Y} {Z} =
     comp-hom-Abstract-Group-Action G X Y Z
   pr2 (pr1 (pr2 (pr2 (Abstract-Group-Action-Precategory l2)))) {X} {Y} {Z} {W} =
diff --git a/src/group-theory/precategory-of-groups.lagda.md b/src/group-theory/precategory-of-groups.lagda.md
index 6a4d7a92d1..ac6f4e4038 100644
--- a/src/group-theory/precategory-of-groups.lagda.md
+++ b/src/group-theory/precategory-of-groups.lagda.md
@@ -23,7 +23,7 @@ open import group-theory.homomorphisms-groups
 instance
   Group-Large-Precategory : Large-Precategory lsuc (_⊔_)
   obj-Large-Precategory Group-Large-Precategory = Group
-  hom-Large-Precategory Group-Large-Precategory = hom-Group
+  hom-set-Large-Precategory Group-Large-Precategory = hom-set-Group
   comp-hom-Large-Precategory Group-Large-Precategory {X = G} {H} {K} =
     comp-hom-Group G H K
   id-hom-Large-Precategory Group-Large-Precategory {X = G} =
diff --git a/src/group-theory/precategory-of-monoids.lagda.md b/src/group-theory/precategory-of-monoids.lagda.md
index 4b3016b332..dda1c7f0cd 100644
--- a/src/group-theory/precategory-of-monoids.lagda.md
+++ b/src/group-theory/precategory-of-monoids.lagda.md
@@ -31,9 +31,9 @@ Monoid-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Monoid-Large-Precategory =
   Monoid
-hom-Large-Precategory
+hom-set-Large-Precategory
   Monoid-Large-Precategory =
-  hom-Monoid
+  hom-set-Monoid
 comp-hom-Large-Precategory
   Monoid-Large-Precategory {X = K} {L} {M} =
   comp-hom-Monoid K L M
diff --git a/src/group-theory/precategory-of-semigroups.lagda.md b/src/group-theory/precategory-of-semigroups.lagda.md
index 238f124e23..6b1a380ec3 100644
--- a/src/group-theory/precategory-of-semigroups.lagda.md
+++ b/src/group-theory/precategory-of-semigroups.lagda.md
@@ -29,7 +29,7 @@ Semigroups and semigroup homomorphisms form a precategory.
 instance
   Semigroup-Large-Precategory : Large-Precategory lsuc (_⊔_)
   obj-Large-Precategory Semigroup-Large-Precategory = Semigroup
-  hom-Large-Precategory Semigroup-Large-Precategory = hom-Semigroup
+  hom-set-Large-Precategory Semigroup-Large-Precategory = hom-set-Semigroup
   comp-hom-Large-Precategory Semigroup-Large-Precategory
     {X = G} {H} {K} =
     comp-hom-Semigroup G H K
diff --git a/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md b/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md
index e4e2af66bd..5ed417a8d1 100644
--- a/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md
+++ b/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md
@@ -343,7 +343,7 @@ module _
         ( H))
 
   subgroup-subset-hom-large-poset-Group :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( λ l2 → l1 ⊔ l2)
       ( powerset-Large-Poset (type-Group G))
       ( Subgroup-Large-Poset G)
diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md
index 927b97ad06..f3a59b454f 100644
--- a/src/group-theory/subgroups.lagda.md
+++ b/src/group-theory/subgroups.lagda.md
@@ -480,7 +480,7 @@ preserves-order-subset-Subgroup G H K = id
 
 subset-subgroup-hom-large-poset-Group :
   {l1 : Level} (G : Group l1) →
-  hom-Large-Poset
+  hom-set-Large-Poset
     ( id)
     ( Subgroup-Large-Poset G)
     ( powerset-Large-Poset (type-Group G))
diff --git a/src/order-theory/closure-operators-large-locales.lagda.md b/src/order-theory/closure-operators-large-locales.lagda.md
index b3d37d8358..7c20d16e68 100644
--- a/src/order-theory/closure-operators-large-locales.lagda.md
+++ b/src/order-theory/closure-operators-large-locales.lagda.md
@@ -63,7 +63,7 @@ module _
     where
 
     hom-large-poset-closure-operator-Large-Locale :
-      hom-Large-Poset id
+      hom-set-Large-Poset id
         ( large-poset-Large-Locale L)
         ( large-poset-Large-Locale L)
     hom-large-poset-closure-operator-Large-Locale =
diff --git a/src/order-theory/closure-operators-large-posets.lagda.md b/src/order-theory/closure-operators-large-posets.lagda.md
index 9badfeef35..2754468f56 100644
--- a/src/order-theory/closure-operators-large-posets.lagda.md
+++ b/src/order-theory/closure-operators-large-posets.lagda.md
@@ -47,7 +47,7 @@ module _
     where
     field
       hom-closure-operator-Large-Poset :
-        hom-Large-Poset id P P
+        hom-set-Large-Poset id P P
       is-inflationary-closure-operator-Large-Poset :
         {l1 : Level} (x : type-Large-Poset P l1) →
         leq-Large-Poset P x
diff --git a/src/order-theory/galois-connections-large-posets.lagda.md b/src/order-theory/galois-connections-large-posets.lagda.md
index 0a2157a3d8..6778055437 100644
--- a/src/order-theory/galois-connections-large-posets.lagda.md
+++ b/src/order-theory/galois-connections-large-posets.lagda.md
@@ -22,8 +22,8 @@ open import order-theory.order-preserving-maps-large-posets
 A **galois connection** between [large posets](order-theory.large-posets.md) `P`
 and `Q` consists of
 [order preserving maps](order-theory.order-preserving-maps-large-posets.md)
-`f : hom-Large-Poset id P Q` and `hom-Large-Poset id Q P` such that the adjoint
-relation
+`f : hom-set-Large-Poset id P Q` and `hom-set-Large-Poset id Q P` such that the
+adjoint relation
 
 ```text
   (f x ≤ y) ↔ (x ≤ g y)
@@ -60,9 +60,9 @@ module _
       make-galois-connection-Large-Poset
     field
       lower-adjoint-galois-connection-Large-Poset :
-        hom-Large-Poset γ P Q
+        hom-set-Large-Poset γ P Q
       upper-adjoint-galois-connection-Large-Poset :
-        hom-Large-Poset δ Q P
+        hom-set-Large-Poset δ Q P
       adjoint-relation-galois-connection-Large-Poset :
         {l1 l2 : Level}
         (x : type-Large-Poset P l1) (y : type-Large-Poset Q l2) →
@@ -139,13 +139,13 @@ module _
       UU (βQ l1 l2)
     _≤-Q_ = leq-Large-Poset Q
 
-    hom-f : hom-Large-Poset _ P Q
+    hom-f : hom-set-Large-Poset _ P Q
     hom-f = lower-adjoint-galois-connection-Large-Poset G
 
     f : {l : Level} → type-Large-Poset P l → type-Large-Poset Q (γ l)
     f = map-hom-Large-Poset P Q hom-f
 
-    hom-g : hom-Large-Poset _ Q P
+    hom-g : hom-set-Large-Poset _ Q P
     hom-g = upper-adjoint-galois-connection-Large-Poset G
 
     g : {l : Level} → type-Large-Poset Q l → type-Large-Poset P (δ l)
diff --git a/src/order-theory/homomorphisms-large-frames.lagda.md b/src/order-theory/homomorphisms-large-frames.lagda.md
index 80de9de25d..441c3fb91d 100644
--- a/src/order-theory/homomorphisms-large-frames.lagda.md
+++ b/src/order-theory/homomorphisms-large-frames.lagda.md
@@ -33,11 +33,11 @@ module _
   where
 
   record
-    hom-Large-Frame : UUω
+    hom-set-Large-Frame : UUω
     where
     field
       hom-large-meet-semilattice-hom-Large-Frame :
-        hom-Large-Meet-Semilattice
+        hom-set-Large-Meet-Semilattice
           ( large-meet-semilattice-Large-Frame K)
           ( large-meet-semilattice-Large-Frame L)
       preserves-sup-hom-Large-Frame :
@@ -47,10 +47,10 @@ module _
           ( hom-large-poset-hom-Large-Meet-Semilattice
             ( hom-large-meet-semilattice-hom-Large-Frame))
 
-  open hom-Large-Frame public
+  open hom-set-Large-Frame public
 
   module _
-    (f : hom-Large-Frame)
+    (f : hom-set-Large-Frame)
     where
 
     map-hom-Large-Frame :
diff --git a/src/order-theory/homomorphisms-large-locales.lagda.md b/src/order-theory/homomorphisms-large-locales.lagda.md
index ae621fd45d..eb64ab8e8f 100644
--- a/src/order-theory/homomorphisms-large-locales.lagda.md
+++ b/src/order-theory/homomorphisms-large-locales.lagda.md
@@ -30,11 +30,11 @@ module _
   (K : Large-Locale αK βK γ) (L : Large-Locale αL βL γ)
   where
 
-  hom-Large-Locale : UUω
-  hom-Large-Locale = hom-Large-Frame L K
+  hom-set-Large-Locale : UUω
+  hom-set-Large-Locale = hom-set-Large-Frame L K
 
   module _
-    (f : hom-Large-Locale)
+    (f : hom-set-Large-Locale)
     where
 
     map-hom-Large-Locale :
diff --git a/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md b/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md
index dc3ab7fdc7..58ba75386a 100644
--- a/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md
+++ b/src/order-theory/homomorphisms-large-meet-semilattices.lagda.md
@@ -35,11 +35,11 @@ module _
   where
 
   record
-    hom-Large-Meet-Semilattice : UUω
+    hom-set-Large-Meet-Semilattice : UUω
     where
     field
       hom-large-poset-hom-Large-Meet-Semilattice :
-        hom-Large-Poset id
+        hom-set-Large-Poset id
           ( large-poset-Large-Meet-Semilattice K)
           ( large-poset-Large-Meet-Semilattice L)
       preserves-meets-hom-Large-Meet-Semilattice :
@@ -70,10 +70,10 @@ module _
           ( top-Large-Meet-Semilattice K) ＝
         top-Large-Meet-Semilattice L
 
-  open hom-Large-Meet-Semilattice public
+  open hom-set-Large-Meet-Semilattice public
 
   module _
-    (f : hom-Large-Meet-Semilattice)
+    (f : hom-set-Large-Meet-Semilattice)
     where
 
     map-hom-Large-Meet-Semilattice :
diff --git a/src/order-theory/homomorphisms-large-suplattices.lagda.md b/src/order-theory/homomorphisms-large-suplattices.lagda.md
index e0bdab126f..d13f3b7102 100644
--- a/src/order-theory/homomorphisms-large-suplattices.lagda.md
+++ b/src/order-theory/homomorphisms-large-suplattices.lagda.md
@@ -35,7 +35,7 @@ module _
   where
 
   preserves-sup-hom-Large-Poset :
-    hom-Large-Poset id
+    hom-set-Large-Poset id
       ( large-poset-Large-Suplattice K)
       ( large-poset-Large-Suplattice L) →
     UUω
@@ -55,20 +55,20 @@ module _
           ( x i))
 
   record
-    hom-Large-Suplattice : UUω
+    hom-set-Large-Suplattice : UUω
     where
     field
       hom-large-poset-hom-Large-Suplattice :
-        hom-Large-Poset id
+        hom-set-Large-Poset id
           ( large-poset-Large-Suplattice K)
           ( large-poset-Large-Suplattice L)
       preserves-sup-hom-Large-Suplattice :
         preserves-sup-hom-Large-Poset hom-large-poset-hom-Large-Suplattice
 
-  open hom-Large-Suplattice public
+  open hom-set-Large-Suplattice public
 
   module _
-    (f : hom-Large-Suplattice)
+    (f : hom-set-Large-Suplattice)
     where
 
     map-hom-Large-Suplattice :
diff --git a/src/order-theory/homomorphisms-meet-semilattices.lagda.md b/src/order-theory/homomorphisms-meet-semilattices.lagda.md
index b65d7cfb7a..e0abeac2dc 100644
--- a/src/order-theory/homomorphisms-meet-semilattices.lagda.md
+++ b/src/order-theory/homomorphisms-meet-semilattices.lagda.md
@@ -61,15 +61,15 @@ module _
       ( semigroup-Meet-Semilattice A)
       ( semigroup-Meet-Semilattice B)
 
-  hom-Meet-Semilattice : Set (l1 ⊔ l2)
-  hom-Meet-Semilattice =
-    hom-Semigroup (semigroup-Meet-Semilattice A) (semigroup-Meet-Semilattice B)
+  hom-set-Meet-Semilattice : Set (l1 ⊔ l2)
+  hom-set-Meet-Semilattice =
+    hom-set-Semigroup (semigroup-Meet-Semilattice A) (semigroup-Meet-Semilattice B)
 
   type-hom-Meet-Semilattice : UU (l1 ⊔ l2)
-  type-hom-Meet-Semilattice = type-Set hom-Meet-Semilattice
+  type-hom-Meet-Semilattice = type-Set hom-set-Meet-Semilattice
 
   is-set-type-hom-Meet-Semilattice : is-set type-hom-Meet-Semilattice
-  is-set-type-hom-Meet-Semilattice = is-set-type-Set hom-Meet-Semilattice
+  is-set-type-hom-Meet-Semilattice = is-set-type-Set hom-set-Meet-Semilattice
 
   module _
     (f : type-hom-Meet-Semilattice)
@@ -140,8 +140,8 @@ module _
   is-prop-preserves-meet-hom-Prop f =
     is-prop-type-Prop (preserves-meet-hom-Poset-Prop f)
 
-  hom-Order-Theoretic-Meet-Semilattice : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  hom-Order-Theoretic-Meet-Semilattice =
+  hom-set-Order-Theoretic-Meet-Semilattice : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-set-Order-Theoretic-Meet-Semilattice =
     set-subset
       ( hom-set-Poset
         ( poset-Order-Theoretic-Meet-Semilattice A)
diff --git a/src/order-theory/large-posets.lagda.md b/src/order-theory/large-posets.lagda.md
index 03b60c2766..32715957a5 100644
--- a/src/order-theory/large-posets.lagda.md
+++ b/src/order-theory/large-posets.lagda.md
@@ -118,7 +118,7 @@ module _
     is-large-poset-Large-Category →
     is-antisymmetric-Large-Relation
       ( obj-Large-Category C)
-      ( type-hom-Large-Category C)
+      ( hom-Large-Category C)
   is-antisymmetric-is-large-poset-Large-Category H X Y f g =
     eq-iso-Large-Category C X Y
       ( f , g , eq-is-prop (H Y Y) , eq-is-prop (H X X))
diff --git a/src/order-theory/large-preorders.lagda.md b/src/order-theory/large-preorders.lagda.md
index ba9c1b5721..cb7beffe4d 100644
--- a/src/order-theory/large-preorders.lagda.md
+++ b/src/order-theory/large-preorders.lagda.md
@@ -88,7 +88,7 @@ module _
   is-large-preorder-Large-Precategory =
     {l1 l2 : Level}
     (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2) →
-    is-prop (type-hom-Large-Precategory C X Y)
+    is-prop (hom-Large-Precategory C X Y)
 
   large-preorder-Large-Precategory :
     is-large-preorder-Large-Precategory → Large-Preorder α β
@@ -96,7 +96,7 @@ module _
     ( large-preorder-Large-Precategory H) =
     obj-Large-Precategory C
   pr1 (leq-prop-Large-Preorder (large-preorder-Large-Precategory H) X Y) =
-    type-hom-Large-Precategory C X Y
+    hom-Large-Precategory C X Y
   pr2 (leq-prop-Large-Preorder (large-preorder-Large-Precategory H) X Y) =
     H X Y
   refl-leq-Large-Preorder
@@ -136,7 +136,7 @@ module _
 
   large-precategory-Large-Preorder : Large-Precategory α β
   obj-Large-Precategory large-precategory-Large-Preorder = type-Large-Preorder P
-  hom-Large-Precategory large-precategory-Large-Preorder x y =
+  hom-set-Large-Precategory large-precategory-Large-Preorder x y =
     set-Prop (leq-prop-Large-Preorder P x y)
   comp-hom-Large-Precategory large-precategory-Large-Preorder {X = x} {y} {z} =
     transitive-leq-Large-Preorder P x y z
diff --git a/src/order-theory/nuclei-large-locales.lagda.md b/src/order-theory/nuclei-large-locales.lagda.md
index 3c68074c01..f4e94f161b 100644
--- a/src/order-theory/nuclei-large-locales.lagda.md
+++ b/src/order-theory/nuclei-large-locales.lagda.md
@@ -35,8 +35,8 @@ open import order-theory.least-upper-bounds-large-posets
 ## Idea
 
 A **nucleus** on a [large locale](order-theory.large-locales.md) `L` is an order
-preserving map `j : hom-Large-Poset id L L` such that `j` preserves meets and is
-inflationary and idempotent.
+preserving map `j : hom-set-Large-Poset id L L` such that `j` preserves meets
+and is inflationary and idempotent.
 
 ## Definitions
 
@@ -53,7 +53,7 @@ module _
     where
     field
       hom-large-meet-semilattice-nucleus-Large-Locale :
-        hom-Large-Meet-Semilattice
+        hom-set-Large-Meet-Semilattice
           ( large-meet-semilattice-Large-Locale L)
           ( large-meet-semilattice-Large-Locale L)
       is-inflationary-nucleus-Large-Locale :
diff --git a/src/order-theory/order-preserving-maps-large-posets.lagda.md b/src/order-theory/order-preserving-maps-large-posets.lagda.md
index 77a3f65076..e1e1280218 100644
--- a/src/order-theory/order-preserving-maps-large-posets.lagda.md
+++ b/src/order-theory/order-preserving-maps-large-posets.lagda.md
@@ -35,16 +35,16 @@ module _
   (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
   where
 
-  hom-Large-Poset : UUω
-  hom-Large-Poset =
-    hom-Large-Preorder γ
+  hom-set-Large-Poset : UUω
+  hom-set-Large-Poset =
+    hom-set-Large-Preorder γ
       ( large-preorder-Large-Poset P)
       ( large-preorder-Large-Poset Q)
 
 module _
   {αP αQ : Level → Level} {βP βQ : Level → Level → Level} {γ : Level → Level}
   (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
-  (f : hom-Large-Poset γ P Q)
+  (f : hom-set-Large-Poset γ P Q)
   where
 
   map-hom-Large-Poset :
diff --git a/src/order-theory/order-preserving-maps-large-preorders.lagda.md b/src/order-theory/order-preserving-maps-large-preorders.lagda.md
index 2f27a3f10d..825ab09970 100644
--- a/src/order-theory/order-preserving-maps-large-preorders.lagda.md
+++ b/src/order-theory/order-preserving-maps-large-preorders.lagda.md
@@ -35,7 +35,7 @@ module _
   (P : Large-Preorder αP βP) (Q : Large-Preorder αQ βQ)
   where
 
-  record hom-Large-Preorder : UUω
+  record hom-set-Large-Preorder : UUω
     where
     constructor
       make-hom-Large-Preorder
@@ -51,5 +51,5 @@ module _
           ( map-hom-Large-Preorder x)
           ( map-hom-Large-Preorder y)
 
-  open hom-Large-Preorder public
+  open hom-set-Large-Preorder public
 ```
diff --git a/src/order-theory/posets.lagda.md b/src/order-theory/posets.lagda.md
index e4e97f6597..2123e07862 100644
--- a/src/order-theory/posets.lagda.md
+++ b/src/order-theory/posets.lagda.md
@@ -168,7 +168,7 @@ module _
 module _
   {l1 l2 : Level} (C : Category l1 l2)
   ( is-prop-hom-C :
-    (x y : obj-Category C) → is-prop (type-hom-Category C x y))
+    (x y : obj-Category C) → is-prop (hom-Category C x y))
   where
 
   preorder-is-prop-hom-Category : Preorder l1 l2
diff --git a/src/order-theory/preorders.lagda.md b/src/order-theory/preorders.lagda.md
index 971bbf4ea6..ea639bd1bd 100644
--- a/src/order-theory/preorders.lagda.md
+++ b/src/order-theory/preorders.lagda.md
@@ -151,14 +151,14 @@ module _
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   ( is-prop-hom-C :
-    (x y : obj-Precategory C) → is-prop (type-hom-Precategory C x y))
+    (x y : obj-Precategory C) → is-prop (hom-Precategory C x y))
   where
 
   preorder-is-prop-hom-Precategory : Preorder l1 l2
   pr1 preorder-is-prop-hom-Precategory =
     obj-Precategory C
   pr1 (pr1 (pr2 preorder-is-prop-hom-Precategory) x y) =
-    type-hom-Precategory C x y
+    hom-Precategory C x y
   pr2 (pr1 (pr2 preorder-is-prop-hom-Precategory) x y) =
     is-prop-hom-C x y
   pr1 (pr2 (pr2 preorder-is-prop-hom-Precategory)) x =
diff --git a/src/order-theory/reflective-galois-connections-large-posets.lagda.md b/src/order-theory/reflective-galois-connections-large-posets.lagda.md
index bd27be52af..a55d6c14fc 100644
--- a/src/order-theory/reflective-galois-connections-large-posets.lagda.md
+++ b/src/order-theory/reflective-galois-connections-large-posets.lagda.md
@@ -71,7 +71,7 @@ module _
     where
 
     lower-adjoint-reflective-galois-connection-Large-Poset :
-      hom-Large-Poset γ P Q
+      hom-set-Large-Poset γ P Q
     lower-adjoint-reflective-galois-connection-Large-Poset =
       lower-adjoint-galois-connection-Large-Poset
         ( galois-connection-reflective-galois-connection-Large-Poset G)
diff --git a/src/reflection/precategory-solver.lagda.md b/src/reflection/precategory-solver.lagda.md
index b45e0a41d7..95f866533d 100644
--- a/src/reflection/precategory-solver.lagda.md
+++ b/src/reflection/precategory-solver.lagda.md
@@ -61,9 +61,9 @@ module _
     where
     id-hom-Precategory-Expr :
       {x : obj-Precategory C} → Precategory-Expr x x
-    type-hom-Precategory-Expr :
+    hom-Precategory-Expr :
       {x y : obj-Precategory C} →
-      type-hom-Precategory C x y → Precategory-Expr x y
+      hom-Precategory C x y → Precategory-Expr x y
     comp-hom-Precategory-Expr :
       {x y z : obj-Precategory C} →
       Precategory-Expr y z → Precategory-Expr x y → Precategory-Expr x z
@@ -75,9 +75,9 @@ module _
   in-Precategory-Expr :
     {x y : obj-Precategory C} →
     Precategory-Expr x y →
-    type-hom-Precategory C x y
+    hom-Precategory C x y
   in-Precategory-Expr id-hom-Precategory-Expr = id-hom-Precategory C
-  in-Precategory-Expr (type-hom-Precategory-Expr f) = f
+  in-Precategory-Expr (hom-Precategory-Expr f) = f
   in-Precategory-Expr (comp-hom-Precategory-Expr f g) =
     comp-hom-Precategory C (in-Precategory-Expr f) (in-Precategory-Expr g)
 ```
@@ -88,10 +88,10 @@ module _
   eval-Precategory-Expr :
     {x y z : obj-Precategory C} →
     Precategory-Expr y z →
-    type-hom-Precategory C x y →
-    type-hom-Precategory C x z
+    hom-Precategory C x y →
+    hom-Precategory C x z
   eval-Precategory-Expr id-hom-Precategory-Expr f = f
-  eval-Precategory-Expr (type-hom-Precategory-Expr f) g =
+  eval-Precategory-Expr (hom-Precategory-Expr f) g =
     comp-hom-Precategory C f g
   eval-Precategory-Expr (comp-hom-Precategory-Expr f g) h =
     eval-Precategory-Expr f (eval-Precategory-Expr g h)
@@ -99,12 +99,12 @@ module _
   is-sound-eval-Precategory-Expr :
     {x y z : obj-Precategory C}
     (e : Precategory-Expr y z)
-    (f : type-hom-Precategory C x y) →
+    (f : hom-Precategory C x y) →
     ( eval-Precategory-Expr e f) ＝
     ( comp-hom-Precategory C (in-Precategory-Expr e) f)
   is-sound-eval-Precategory-Expr id-hom-Precategory-Expr f =
     inv (left-unit-law-comp-hom-Precategory C f)
-  is-sound-eval-Precategory-Expr (type-hom-Precategory-Expr f) g = refl
+  is-sound-eval-Precategory-Expr (hom-Precategory-Expr f) g = refl
   is-sound-eval-Precategory-Expr (comp-hom-Precategory-Expr f g) h =
     equational-reasoning
     eval-Precategory-Expr f (eval-Precategory-Expr g h)
@@ -131,7 +131,7 @@ module _
   normalize-Precategory-Expr :
     {x y : obj-Precategory C} →
     Precategory-Expr x y →
-    type-hom-Precategory C x y
+    hom-Precategory C x y
   normalize-Precategory-Expr e = eval-Precategory-Expr e (id-hom-Precategory C)
 
   is-sound-normalize-Precategory-Expr :
@@ -190,7 +190,7 @@ private
         xs)
 ```
 
-### Building a term of `Precategory-Expr C x y` from a term of type `type-hom-Precategory C x y`
+### Building a term of `Precategory-Expr C x y` from a term of type `hom-Precategory C x y`
 
 ```agda
 build-Precategory-Expr : Term → Term
@@ -225,7 +225,7 @@ build-Precategory-Expr
       visible-Arg (build-Precategory-Expr f) ∷
       nil)
 build-Precategory-Expr f =
-  con (quote type-hom-Precategory-Expr) (visible-Arg f ∷ nil)
+  con (quote hom-Precategory-Expr) (visible-Arg f ∷ nil)
 ```
 
 ### The application of the `solve-Precategory-Expr` lemma
@@ -268,7 +268,7 @@ module _
   private
     _ :
       {x y : obj-Precategory C}
-      {f : type-hom-Precategory C x y} →
+      {f : hom-Precategory C x y} →
       f ＝ f
     _ = solve-Precategory! C
 
@@ -279,26 +279,26 @@ module _
 
     _ :
       {a b c : obj-Precategory C}
-      {f : type-hom-Precategory C a b}
-      {g : type-hom-Precategory C b c} →
+      {f : hom-Precategory C a b}
+      {g : hom-Precategory C b c} →
       (comp-hom-Precategory C g f) ＝
       comp-hom-Precategory C g f
     _ = solve-Precategory! C
 
     _ :
       {a b c d : obj-Precategory C}
-      {f : type-hom-Precategory C a b}
-      {g : type-hom-Precategory C b c} →
-      {h : type-hom-Precategory C c d} →
+      {f : hom-Precategory C a b}
+      {g : hom-Precategory C b c} →
+      {h : hom-Precategory C c d} →
       comp-hom-Precategory C h (comp-hom-Precategory C g f) ＝
       comp-hom-Precategory C (comp-hom-Precategory C h g) f
     _ = solve-Precategory! C
 
     _ :
       {a b c d : obj-Precategory C}
-      {f : type-hom-Precategory C a b}
-      {g : type-hom-Precategory C b c} →
-      {h : type-hom-Precategory C c d} →
+      {f : hom-Precategory C a b}
+      {g : hom-Precategory C b c} →
+      {h : hom-Precategory C c d} →
       comp-hom-Precategory C
         ( comp-hom-Precategory C h (id-hom-Precategory C))
         ( comp-hom-Precategory C g f) ＝
diff --git a/src/ring-theory/category-of-cyclic-rings.lagda.md b/src/ring-theory/category-of-cyclic-rings.lagda.md
index 2ff55e4845..8f0f1a3155 100644
--- a/src/ring-theory/category-of-cyclic-rings.lagda.md
+++ b/src/ring-theory/category-of-cyclic-rings.lagda.md
@@ -47,9 +47,9 @@ Cyclic-Ring-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Cyclic-Ring-Large-Precategory =
   Cyclic-Ring
-hom-Large-Precategory
+hom-set-Large-Precategory
   Cyclic-Ring-Large-Precategory =
-  hom-Cyclic-Ring
+  hom-set-Cyclic-Ring
 comp-hom-Large-Precategory
   Cyclic-Ring-Large-Precategory {X = R} {Y = S} {Z = T} =
   comp-hom-Cyclic-Ring R S T
diff --git a/src/ring-theory/free-rings-with-one-generator.lagda.md b/src/ring-theory/free-rings-with-one-generator.lagda.md
index 7e7cb1ab55..4131005dfa 100644
--- a/src/ring-theory/free-rings-with-one-generator.lagda.md
+++ b/src/ring-theory/free-rings-with-one-generator.lagda.md
@@ -23,7 +23,7 @@ The **free ring with one generator** is specified as a
 every ring `S` the map
 
 ```text
-  hom-Ring R S → type-Ring S
+  hom-set-Ring R S → type-Ring S
 ```
 
 given by evaluating at the element `g` is an equivalence. This property is also
diff --git a/src/ring-theory/groups-of-units-rings.lagda.md b/src/ring-theory/groups-of-units-rings.lagda.md
index b970a43946..030b58b89b 100644
--- a/src/ring-theory/groups-of-units-rings.lagda.md
+++ b/src/ring-theory/groups-of-units-rings.lagda.md
@@ -248,10 +248,10 @@ module _
 ```agda
 group-of-units-ring-functor-Large-Precategory :
   functor-Large-Precategory Ring-Large-Precategory Group-Large-Precategory id
-obj-functor-Large-Precategory
+map-obj-functor-Large-Precategory
   group-of-units-ring-functor-Large-Precategory =
   group-of-units-Ring
-hom-functor-Large-Precategory
+map-hom-functor-Large-Precategory
   group-of-units-ring-functor-Large-Precategory {X = R} {Y = S} =
   hom-group-of-units-hom-Ring R S
 preserves-comp-functor-Large-Precategory
diff --git a/src/ring-theory/homomorphisms-cyclic-rings.lagda.md b/src/ring-theory/homomorphisms-cyclic-rings.lagda.md
index 3d16f34ec8..92248e5768 100644
--- a/src/ring-theory/homomorphisms-cyclic-rings.lagda.md
+++ b/src/ring-theory/homomorphisms-cyclic-rings.lagda.md
@@ -43,8 +43,8 @@ module _
   {l1 l2 : Level} (R : Cyclic-Ring l1) (S : Cyclic-Ring l2)
   where
 
-  hom-Cyclic-Ring : Set (l1 ⊔ l2)
-  hom-Cyclic-Ring = hom-Ring (ring-Cyclic-Ring R) (ring-Cyclic-Ring S)
+  hom-set-Cyclic-Ring : Set (l1 ⊔ l2)
+  hom-set-Cyclic-Ring = hom-set-Ring (ring-Cyclic-Ring R) (ring-Cyclic-Ring S)
 
   type-hom-Cyclic-Ring : UU (l1 ⊔ l2)
   type-hom-Cyclic-Ring = type-hom-Ring (ring-Cyclic-Ring R) (ring-Cyclic-Ring S)
diff --git a/src/ring-theory/homomorphisms-rings.lagda.md b/src/ring-theory/homomorphisms-rings.lagda.md
index ae5f15cdfe..57ca9c69e5 100644
--- a/src/ring-theory/homomorphisms-rings.lagda.md
+++ b/src/ring-theory/homomorphisms-rings.lagda.md
@@ -119,17 +119,17 @@ module _
   {l1 l2 : Level} (R : Ring l1) (S : Ring l2)
   where
 
-  hom-Ring : Set (l1 ⊔ l2)
-  hom-Ring =
+  hom-set-Ring : Set (l1 ⊔ l2)
+  hom-set-Ring =
     set-subset
-      ( hom-Ab (ab-Ring R) (ab-Ring S))
+      ( hom-set-Ab (ab-Ring R) (ab-Ring S))
       ( is-ring-homomorphism-hom-Ab-Prop R S)
 
   type-hom-Ring : UU (l1 ⊔ l2)
-  type-hom-Ring = type-Set hom-Ring
+  type-hom-Ring = type-Set hom-set-Ring
 
   is-set-type-hom-Ring : is-set type-hom-Ring
-  is-set-type-hom-Ring = is-set-type-Set hom-Ring
+  is-set-type-hom-Ring = is-set-type-Set hom-set-Ring
 
   module _
     (f : type-hom-Ring)
diff --git a/src/ring-theory/homomorphisms-semirings.lagda.md b/src/ring-theory/homomorphisms-semirings.lagda.md
index 2a531cfb16..ed70af8a1f 100644
--- a/src/ring-theory/homomorphisms-semirings.lagda.md
+++ b/src/ring-theory/homomorphisms-semirings.lagda.md
@@ -79,19 +79,19 @@ module _
   is-prop-is-homomorphism-semiring-hom-Commutative-Monoid f =
     is-prop-type-Prop (is-homomorphism-semiring-hom-Commutative-Monoid-Prop f)
 
-  hom-Semiring : Set (l1 ⊔ l2)
-  hom-Semiring =
+  hom-set-Semiring : Set (l1 ⊔ l2)
+  hom-set-Semiring =
     set-subset
-      ( hom-Commutative-Monoid
+      ( hom-set-Commutative-Monoid
         ( additive-commutative-monoid-Semiring R)
         ( additive-commutative-monoid-Semiring S))
       ( is-homomorphism-semiring-hom-Commutative-Monoid-Prop)
 
   type-hom-Semiring : UU (l1 ⊔ l2)
-  type-hom-Semiring = type-Set hom-Semiring
+  type-hom-Semiring = type-Set hom-set-Semiring
 
   is-set-type-hom-Semiring : is-set type-hom-Semiring
-  is-set-type-hom-Semiring = is-set-type-Set hom-Semiring
+  is-set-type-hom-Semiring = is-set-type-Set hom-set-Semiring
 
   module _
     (f : type-hom-Semiring)
diff --git a/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md
index 9350b7af52..ed5a44efae 100644
--- a/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md
+++ b/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md
@@ -353,7 +353,7 @@ module _
         ( H))
 
   ideal-subset-hom-large-poset-Ring :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( λ l2 → l1 ⊔ l2)
       ( powerset-Large-Poset (type-Ring A))
       ( ideal-Ring-Large-Poset A)
diff --git a/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md
index 2eebe34272..5a23030247 100644
--- a/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md
+++ b/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md
@@ -309,7 +309,7 @@ module _
         ( H))
 
   left-ideal-subset-hom-large-poset-Ring :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( λ l2 → l1 ⊔ l2)
       ( powerset-Large-Poset (type-Ring A))
       ( left-ideal-Ring-Large-Poset A)
diff --git a/src/ring-theory/localizations-rings.lagda.md b/src/ring-theory/localizations-rings.lagda.md
index 8264cb164a..66fdca8c56 100644
--- a/src/ring-theory/localizations-rings.lagda.md
+++ b/src/ring-theory/localizations-rings.lagda.md
@@ -192,9 +192,9 @@ htpy-universal-property-localization-Ring R S T x f H up-f h K =
 {-
 is-equiv-up-localization-up-localization-Ring :
   {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R)
-  (f : hom-Ring R S) (inverts-f : inverts-element-hom-Ring R S x f) →
-  (g : hom-Ring R T) (inverts-g : inverts-element-hom-Ring R T x g) →
-  (h : hom-Ring S T) (H : htpy-hom-Ring R T (comp-hom-Ring R S T h f) g) →
+  (f : hom-set-Ring R S) (inverts-f : inverts-element-hom-Ring R S x f) →
+  (g : hom-set-Ring R T) (inverts-g : inverts-element-hom-Ring R T x g) →
+  (h : hom-set-Ring S T) (H : htpy-hom-Ring R T (comp-hom-Ring R S T h f) g) →
   ({l : Level} → universal-property-localization-Ring l R S x f inverts-f) →
   ({l : Level} → universal-property-localization-Ring l R T x g inverts-g) →
   is-iso-hom-Ring S T h
diff --git a/src/ring-theory/poset-of-ideals-rings.lagda.md b/src/ring-theory/poset-of-ideals-rings.lagda.md
index c75df9d982..8f29c36673 100644
--- a/src/ring-theory/poset-of-ideals-rings.lagda.md
+++ b/src/ring-theory/poset-of-ideals-rings.lagda.md
@@ -151,7 +151,7 @@ module _
   preserves-order-subset-ideal-Ring I J H = H
 
   subset-ideal-hom-large-poset-Ring :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( id)
       ( ideal-Ring-Large-Poset R)
       ( powerset-Large-Poset (type-Ring R))
diff --git a/src/ring-theory/poset-of-left-ideals-rings.lagda.md b/src/ring-theory/poset-of-left-ideals-rings.lagda.md
index 360e5dd3b2..87fda7dfea 100644
--- a/src/ring-theory/poset-of-left-ideals-rings.lagda.md
+++ b/src/ring-theory/poset-of-left-ideals-rings.lagda.md
@@ -161,7 +161,7 @@ module _
   preserves-order-subset-left-ideal-Ring I J H = H
 
   subset-left-ideal-hom-large-poset-Ring :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( id)
       ( left-ideal-Ring-Large-Poset R)
       ( powerset-Large-Poset (type-Ring R))
diff --git a/src/ring-theory/poset-of-right-ideals-rings.lagda.md b/src/ring-theory/poset-of-right-ideals-rings.lagda.md
index c7d7e3ca0d..7911bdafab 100644
--- a/src/ring-theory/poset-of-right-ideals-rings.lagda.md
+++ b/src/ring-theory/poset-of-right-ideals-rings.lagda.md
@@ -162,7 +162,7 @@ module _
   preserves-order-subset-right-ideal-Ring I J H = H
 
   subset-right-ideal-hom-large-poset-Ring :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( id)
       ( right-ideal-Ring-Large-Poset R)
       ( powerset-Large-Poset (type-Ring R))
diff --git a/src/ring-theory/precategory-of-rings.lagda.md b/src/ring-theory/precategory-of-rings.lagda.md
index d95f46a310..4be0085e01 100644
--- a/src/ring-theory/precategory-of-rings.lagda.md
+++ b/src/ring-theory/precategory-of-rings.lagda.md
@@ -32,9 +32,9 @@ Ring-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Ring-Large-Precategory =
   Ring
-hom-Large-Precategory
+hom-set-Large-Precategory
   Ring-Large-Precategory =
-  hom-Ring
+  hom-set-Ring
 comp-hom-Large-Precategory
   Ring-Large-Precategory {X = R} {S} {T} =
   comp-hom-Ring R S T
diff --git a/src/ring-theory/precategory-of-semirings.lagda.md b/src/ring-theory/precategory-of-semirings.lagda.md
index 44c8d9152c..e0ef395d6b 100644
--- a/src/ring-theory/precategory-of-semirings.lagda.md
+++ b/src/ring-theory/precategory-of-semirings.lagda.md
@@ -32,9 +32,9 @@ Semiring-Large-Precategory : Large-Precategory lsuc _⊔_
 obj-Large-Precategory
   Semiring-Large-Precategory =
   Semiring
-hom-Large-Precategory
+hom-set-Large-Precategory
   Semiring-Large-Precategory =
-  hom-Semiring
+  hom-set-Semiring
 comp-hom-Large-Precategory
   Semiring-Large-Precategory {X = R} {S} {T} =
   comp-hom-Semiring R S T
diff --git a/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md
index 38d5ceeffb..1bd74b6b2b 100644
--- a/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md
+++ b/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md
@@ -307,7 +307,7 @@ module _
         ( H))
 
   right-ideal-subset-hom-large-poset-Ring :
-    hom-Large-Poset
+    hom-set-Large-Poset
       ( λ l2 → l1 ⊔ l2)
       ( powerset-Large-Poset (type-Ring A))
       ( right-ideal-Ring-Large-Poset A)
diff --git a/src/species/precategory-of-finite-species.lagda.md b/src/species/precategory-of-finite-species.lagda.md
index 8593d18d98..1144d9a662 100644
--- a/src/species/precategory-of-finite-species.lagda.md
+++ b/src/species/precategory-of-finite-species.lagda.md
@@ -29,7 +29,7 @@ species-𝔽-Large-Precategory :
   (l1 : Level) →
   Large-Precategory (λ l → lsuc l1 ⊔ lsuc l) (λ l2 l3 → lsuc l1 ⊔ l2 ⊔ l3)
 obj-Large-Precategory (species-𝔽-Large-Precategory l1) = species-𝔽 l1
-hom-Large-Precategory (species-𝔽-Large-Precategory l1) = hom-species-𝔽
+hom-set-Large-Precategory (species-𝔽-Large-Precategory l1) = hom-species-𝔽
 comp-hom-Large-Precategory (species-𝔽-Large-Precategory l1) {X = F} {G} {H} =
   comp-hom-species-𝔽 F G H
 id-hom-Large-Precategory (species-𝔽-Large-Precategory l1) {X = F} =