[Agda] 'categories' library in 2.5.1.1

[Jacques Carette]

I'll clean up my fixes for the easy stuff (which are indeed due to the 
changed import conventions) and push them to a clean branch on my fork.  
Once I know who is interested in helping, I'll take this off-list.

Then all of these fixes can be packaged up as a pull request for [1].

Jacques

On 2016-11-02 13:01 , Andreas Abel wrote:
> 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
>
>