From f5dded9561fdf30f69a3b3864b58d3a293586d8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 16:41:17 +0100
Subject: [PATCH] Do not use IsCategory directly

---
 src/Cat/Category/Functor.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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 ]