From 3032dc61303522e9bbe2561be96e5081dd8af68c 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 10:36:59 +0100
Subject: [PATCH] Make explicit argument

---
 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 484cfdc..b9e72b4 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -50,7 +50,7 @@ open Functor
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}
-    {F : RawFunctor ℂ 𝔻}
+    (F : RawFunctor ℂ 𝔻)
     where
   private
     module 𝔻 = IsCategory (isCategory 𝔻)
@@ -77,7 +77,7 @@ module _
 
   IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
   IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
-    (\ F → propIsFunctor {F = F}) (\ i → F i)
+    (\ F → propIsFunctor F) (\ i → F i)
     where
       open import Cubical.NType.Properties using (lemPropF)