[Agda] 'categories' library in 2.5.1.1

[Andreas Abel]

I cloned [1], but type-checking fails already at

/home/abel/project/open-source/categories/Categories/Morphisms.agda:175,8-12
Duplicate definition of module _∼ⁱ_. Previous definition of
datatype module _∼ⁱ_ at
/home/abel/project/open-source/categories/Categories/Category.agda:127,8-11
when scope checking the declaration
   module _∼ⁱ_ {A}{B}{i : A ≅ B}{A′}{B′}{j : A′ ≅ B′}
               (eq : i ∼ⁱ j) where

This error is likely due to the changed import conventions for 
data/record modules.

Maybe once the easy problems are fixed, we can make a concerted effort 
to get the hard ones through...  (to avoid duplicate work).

Best,
Andreas

On 02.11.2016 16:14, Jacques Carette wrote:
> I am a heavy user of the wonderful categories [1] library.  But I now
> find that lots of this code is broken in 2.5.1.1.  I have fixed some
> issues in my fork, but I have hit issues (notably in
> Categories.NaturalIsomorphisms) which I don't know how to fix.
>
> Two questions:
> 1) does anyone have a fork where this is fixed?
> 2) if not, would there be a group interested in working with me to do so?
>
> Jacques
>
> [1] https://github.com/copumpkin/categories
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/