diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 0269df9..a55e6bd 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -51,7 +51,7 @@ module _
     (F : RawFunctor ℂ 𝔻)
     where
   private
-    module 𝔻 = IsCategory (isCategory 𝔻)
+    module 𝔻 = Category 𝔻
 
   propIsFunctor : isProp (IsFunctor _ _ F)
   propIsFunctor isF0 isF1 i = record
@@ -69,7 +69,7 @@ module _
     {F : I → RawFunctor ℂ 𝔻}
     where
   private
-    module 𝔻 = IsCategory (isCategory 𝔻)
+    module 𝔻 = Category 𝔻
   IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
   IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]