diff --git a/Modules/Prelims/EpiComplements.v b/Modules/Prelims/EpiComplements.v
index f88c5c7..7224782 100644
--- a/Modules/Prelims/EpiComplements.v
+++ b/Modules/Prelims/EpiComplements.v
@@ -175,7 +175,7 @@ Lemma isEpi_horcomp_pw (B : category)(C D : category)
       (G H : functor B C) (G' H' : functor C D)
       (f : nat_trans G H) (f':nat_trans G' H')
   : (∏ x, isEpi  (f' x))
-    -> (∏ x, isEpi ((# H')%Cat (f x)))
+    -> (∏ x, isEpi ((# H') (f x)))
     -> ∏ x,  isEpi (horcomp f f' x).
 Proof.
   intros epif' epif.
@@ -189,7 +189,7 @@ Lemma isEpi_horcomp_pw2 (B : category)(C D : category)
       (G H : functor B C) (G' H' : functor C D)
       (f : nat_trans G H) (f':nat_trans G' H')
   : (∏ x, isEpi  (f' x))
-    -> (∏ x, isEpi ((# G')%Cat (f x)))
+    -> (∏ x, isEpi ((# G') (f x)))
     -> ∏ x,  isEpi (horcomp f f' x).
 Proof.
   intros epif epif'.
@@ -211,7 +211,7 @@ If the source category B is Set, then with the axiom of choice every epimorphism
 thus absolute (i.e. any functor preserves epis).
 *)
 Definition preserves_Epi {B C : precategory} (F : functor B C) : UU :=
-  ∏ a b (f : B ⟦a , b⟧), isEpi  f -> isEpi (# F f)%Cat.
+  ∏ a b (f : B ⟦a , b⟧), isEpi  f -> isEpi (# F f).
 
 (** Functor from Set preserves epimorphisms because thanks to the axiom of choice, any
     set epimorphism is absolute *)
diff --git a/Modules/Prelims/lib.v b/Modules/Prelims/lib.v
index 32fdd5d..9aa4609 100644
--- a/Modules/Prelims/lib.v
+++ b/Modules/Prelims/lib.v
@@ -137,9 +137,9 @@ Qed.
 
 (** Same as [nat_trans_comp_pointwise], but with B = A · A' *)
 Definition nat_trans_comp_pointwise' :
-  ∏ (C : precategory) (C' : category)  (F G H : ([C, C' , _ ])%Cat)
-    (A : ([C, C' , _] ⟦ F, G ⟧)%Cat) (A' : ([C, C' , _] ⟦ G, H ⟧)%Cat) (a : C),
-  ((A  : nat_trans _ _) a ·  (A' : nat_trans _ _) a)%Cat =  (A · A' : nat_trans _ _)%Cat a
+  ∏ (C : precategory) (C' : category)  (F G H : ([C, C' , _ ]))
+    (A : ([C, C' , _] ⟦ F, G ⟧)) (A' : ([C, C' , _] ⟦ G, H ⟧)) (a : C),
+  ((A  : nat_trans _ _) a ·  (A' : nat_trans _ _) a) =  (A · A' : nat_trans _ _) a
   :=
   fun C C'  F G H A A' => @nat_trans_comp_pointwise C C' (homset_property C') F G H A A' _ (idpath _).