The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there any particular reason you want to use the ConCat library, rather than a more recent category theory library?  There are many of them (http://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants), including my own; I have an older version of my library at https://bitbucket.org/JasonGross/catdb/src for Coq 8.4, and a newer (and semi-actively developed) version at https://github.com/HoTT/HoTT/tree/master/theories/categories for HoTT/coq.

-Jason

On Wed, Feb 12, 2014 at 12:32 AM, monde wilson <wilsonmonde AT gmail.com> wrote:

is there any example about using ConCat library