Find/Make a Category Theory Library

[Lysxia]

Everything in the library under Basics really belongs in its own library. A huge chunk of that is a whole category theory library.

The next step is to review existing implementations to see whether any one is compatible with what we are doing. Luckily, a recent discussion on the Coq Discourse forum gives a list of them: https://coq.discourse.group/t/survey-of-category-theory-in-coq/371

A related question I have is whether the Monad class from ext-lib can be replaced with a more general class formalizing monads in arbitrary categories (ext-lib's Monad is specialized to the category of functions). Two big sticking points that make such unification difficult are (1) going back and forth between "monadic" and "categorical" notation (for both reasoning and programming), (2) extraction to OCaml, a call-by-value and impure language, where eta-reduction and other pointfree shenanigans significantly impact semantics and performance. (We could also give up (2) and extract to Haskell but then interoperability with QuickChick (which we haven't worked out yet) becomes more difficult...)

[euisuny]

Hi Li-Yao! A similar concern came up while trying to work on PropT, so I also started here to attempt generalizing a monad definition to arbitrary categories. It's roughly based on ITree's CategoryFunctor.v, ext-lib's monad definition, and @jwiegley's category theory formalization of monads.

For convenience, I've defined the laws we need for ""practical reasons"", but it doesn't have all the theory behind monads. I was curious if there's been progress on this thread---is this work on finding/making category theory library ongoing somewhere?

[Lysxia]

I haven't gotten around to investigate this yet!

[YaZko]

There's also some additional definitions about opposite categories, dagger categories and products that I defined last month in this branch. Nothing fancy but we may want to merge them in at some point.