The Coq mailing list

[Faré <fahree AT gmail.com>]

Dear Coq clubbers,

I haven't done any Coq in ~15 years, but would like to use it to
formalize some trivial theories about operational semantics as
categories, first-class implementations as profunctors between these
categories, and full abstraction between these implementations
equipped with extra properties, as part of my resurrected thesis (if
anyone is interested in these topics, see ch. 2-5 of my thesis draft
at http://fare.tunes.org/tmp/phd/thesis.pdf for a mock-up in Agda of
the properties I'd like to formalize and prove).

Is there a good implementation of category theory in Coq that:
1- Allows for category laws up to some explicit equivalence relation?
2- Uses type classes or something equivalent to incrementally discuss
implementations with or without a variety of additional properties?
(e.g. variants of Totality, Liveness, Co-Liveness, commutativity of
diagrams involving some observation functors, etc.)
3- If possible allows for short-hand notation using Unicode
characters? (I'd like to use plenty of fancy arrows to distinguish the
various of kinds of "morphisms" or "(pro)functors" at stake and their
(dis)allowed side-effects.

If these things already exists in Coq, but requires any technique
added to Coq in the last 15 years, is there a good tutorial for how to
use them?

A quick search finds this, but there is about no documentation on how
to use it, much less modify it:
https://github.com/JasonGross/HoTT/tree/master/theories/categories

I don't need any deep theorems, but at the same time I'd like if
possible to not reinvent everything about Category Theory, and maybe
even interoperate with other libraries for operational semantics.

—♯ƒ • François-René ÐVB Rideau •Reflection&Cybernethics• http://fare.tunes.org
Jésus avait peut-être raison quand il a dit que les pauvres hériteront de la
terre — mais ils en héritent par petits lots de deux mêtres carrés.
       — Robert Heinlein