Make explicit argument
This commit is contained in:
parent
cc1ddaac9f
commit
3032dc6130
|
@ -50,7 +50,7 @@ open Functor
|
||||||
module _
|
module _
|
||||||
{ℓa ℓb : Level}
|
{ℓa ℓb : Level}
|
||||||
{ℂ 𝔻 : Category ℓa ℓb}
|
{ℂ 𝔻 : Category ℓa ℓb}
|
||||||
{F : RawFunctor ℂ 𝔻}
|
(F : RawFunctor ℂ 𝔻)
|
||||||
where
|
where
|
||||||
private
|
private
|
||||||
module 𝔻 = IsCategory (isCategory 𝔻)
|
module 𝔻 = IsCategory (isCategory 𝔻)
|
||||||
|
@ -77,7 +77,7 @@ module _
|
||||||
|
|
||||||
IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
|
IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
|
||||||
IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
|
IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
|
||||||
(\ F → propIsFunctor {F = F}) (\ i → F i)
|
(\ F → propIsFunctor F) (\ i → F i)
|
||||||
where
|
where
|
||||||
open import Cubical.NType.Properties using (lemPropF)
|
open import Cubical.NType.Properties using (lemPropF)
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue