search

pcapriotti / agda-categories

Category theory and algebra
27 stars 3 forks source link

loading zero.agda #1

Open nrolland opened 7 years ago

nrolland commented 7 years ago

Hi,

I was trying to load your library with Agda version 2.5.1, standard library v0.12 and agda-base at 823c684 (2016-06-19) but it could not compile with error

/agda-categories/category/category/zero.agda:13,8-18

No instance of type Coercion (Bundle (IsGraph i j)) (Bundle (IsGraph (_i_6 i j W) (_j_7 i j W))) was found in scope.

It might be a stupid thing on my part, as I did not use agda for some time..

pcapriotti commented 7 years ago

I haven't updated this library in a long time. With the recent changes to instance arguments in Agda, the overloading mechanism that I was using should probably be redesigned and rewritten. It is probably going to require quite a lot of work before it can be typechecked again.

nrolland commented 7 years ago

Is there any way to point to a freezed Agda/Standard lib version which would make it work ?

pcapriotti commented 7 years ago

Probably Agda 2.3.2. The standard lib is irrelevant, because agda-categories does not use it.