[Agda] 'categories' library in 2.5.1.1

[Miëtek Bak]

I tried to fix the categories library a while ago, but ran into some trouble around Categories/Cone.agda.

Here’s my work-in-progress:
https://github.com/mietek/categories/tree/master
https://github.com/mietek/categories/commit/3a3dbc436f131bbf4c0598cd4fe1b5c7403d2b1d


-- 
Miëtek
https://mietek.io




> On 2 Nov 2016, at 18:10, Jacques Carette <carette at mcmaster.ca> wrote:
> 
> 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
>> 
>> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4203 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20161102/e76f67dd/smime.bin