<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Hi, Clarissa.<div><br></div><div>I am not sure of a chosen formalization. I have one that I am using to formalize my work in</div><div>categorical logic. You can find what I have so far here:</div><div><br></div><div><a href="https://github.com/heades/law">https://github.com/heades/law</a></div><div><br></div><div>Law is based on setoid's. You can find pointers to the literature in the source files.</div><div><br></div><div>There is also Daniel Peebles' library based on relations:</div><div><br></div><div><a href="https://github.com/copumpkin/categories">https://github.com/copumpkin/categories</a></div><div><br></div><div>I hope this helps!</div><div><br></div><div>Very best regards,<br><div apple-content-edited="true">
.\ Harley<br>
</div>
<br><div><div>On May 14, 2014, at 8:20 PM, Clarissa Littler <<a href="mailto:clarissa.littler@gmail.com">clarissa.littler@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Hi all,<div>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 <a href="http://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants">http://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants</a> ) but I wasn't sure which, if any, was The Chosen One by the community.</div>
<div><br></div><div>Thanks,</div><div>Clarissa</div></div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></div></body></html>