[Agda] Another library question: categories

[Harley D. Eades III]

Hi, Clarissa.

I am not sure of a chosen formalization.  I have one that I am using to formalize my work in
categorical logic.  You can find what I have so far here:

https://github.com/heades/law

Law is based on setoid's.  You can find pointers to the literature in the source files.

There is also Daniel Peebles' library based on relations:

https://github.com/copumpkin/categories

I hope this helps!

Very best regards,
.\ Harley

On May 14, 2014, at 8:20 PM, Clarissa Littler <clarissa.littler at gmail.com> wrote:

> Hi all,
> Thanks for the pointers on my last question about domain theory libraries, and I have a bit of a followup: is there a standard library people have settled on for category theory? I found a few searching (particularly the list here http://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants ) but I wasn't sure which, if any, was The Chosen One by the community.
> 
> Thanks,
> Clarissa
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140514/c8072dbc/attachment.html