fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Do not use IsCategory directly

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 16:41:17 +01:00
parent 39284b8d99
commit f5dded9561
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Cat/Category/Functor.agda
View file

@ -51,7 +51,7 @@ module _
(F : RawFunctor ℂ 𝔻) (F : RawFunctor ℂ 𝔻)
where where
private private
module 𝔻 = IsCategory (isCategory 𝔻) module 𝔻 = Category 𝔻
propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record propIsFunctor isF0 isF1 i = record
@ -69,7 +69,7 @@ module _
{F : I → RawFunctor ℂ 𝔻} {F : I → RawFunctor ℂ 𝔻}
where where
private private
module 𝔻 = IsCategory (isCategory 𝔻) module 𝔻 = Category 𝔻
IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ] IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]