I am interested in doing some category theory in Coq.

I am aware that there are various existing libraries available for doing category theory in Coq, but I would prefer to work in the context of a more general library for mathematics for a few reasons.

- I want to be able to draw on the library's results in my work (for example, to draw on existing math-comp facts about Abelian groups to prove theorems about the category of Abelian groups)
- I want my own work to be more useful to others because it is submitted in the context of an existing library.
- I would like the code review and helpul feedback which comes with submitting to a library

Is there any plans to add basic support for category theory to the math-comp library?

We're combining cat th with math comp in our SSProve library:

https://github.com/SSProve/ssprove/tree/main/theories/Relational

Hi @Patrick Nicodemus , there are no short term (< 6 month) plan to have some category theory compatible with the math-comp library. However, me and a few others do have this ambition for the future (6 month < _ < 4 years). And one of the ways that I privilege is based on this small demo: https://github.com/math-comp/hierarchy-builder/blob/master/examples/cat/cat.v

Thanks @Cyril Cohen , looks really interesting!

@Cyril Cohen I looked at the library / watched your talk on HB / read your paper on HB. You say that the category theory library is some ways out. Is the reason for this that you want to continue developing HB to the point where it is adequate to handle the kinds of mixins/factories arising in category theory and perhaps automatically generate a good notion of homomorphisms between structures?

IIRC the current priority with Hierarchy Builder is to fully port mathcomp to use it. This is still a WIP and can be found here: https://github.com/math-comp/math-comp/pull/733

"a good notion of homomorphism" is also a little tricky to get right. On the face of it, group homomorphisms should preserve unit, composition and inverses, but in practice only composition is needed, since the others can be derived. For monoids, this is no longer the case and both comp and unit need to be preserved.

if you generated the definitions, could you ignore such theorems and let the user prove them?

Right, but then if you later want to reason about group homomorphisms do you include the redundant data or use the learner version?

My point is that formalizing algebraic structures isn't a job for autopilot and some careful definitions are sometimes needed.

The definition of a group morphism should cover the structure with the whole list of properties, but a proposition should give the more useful criterion. Just like the definition of a scalar product contains bilinear and symmetric while the usual proof consists into linearity along a single variable and symmetry. You don't need to prove a norm is positive either ; you can deduce it from homogeneity and the triangle inequality. Examples abound where the definition of something isn't redundancy-free.

Perhaps the automatic morphism definition shouldn't be mandatory? After a structure definition Foo, one could either give a hand-written definition of FooMorphism or just ask for the automatic definition.

Ali Caglayan said:

Right, but then if you later want to reason about group homomorphisms do you include the redundant data or use the learner version?

This is exactly the same thing with the definition of groups, rings, etc. That's why we have mixins and factories. The idiomatic definition can be generated and factories provided to account for the cases where less things are needed. It is true however that some careful design is required, e.g. for `orderType`

with both `le`

and `lt`

one would end up generating a too strong definition of homomorphism (so one should be able to explicitly omit `lt`

in the instance)

I want to start writing some category theory code. I was thinking that in order to increase its usability or compatibility with others, I would try to write some kind of interface for a category and try and prove things about a category through that interface, so that whatever the definition of a category turns out to be later, my code is useful as long as I can equip these categories with that interface, something like what Spitters and van der Weegen do in their paper "Typeclasses for Mathematics in Type Theory." Does anyone have any guidance on this?

It might be a silly question as the definition of a category itself might seem to be an abstract interface, so it would be layering abstract interfaces on abstract interfaces

the methodology in that paper leads to math-classes and stdpp, but those are incompatible with using canonical structures like in math-comp — mostly because TC search does not understand canonical structures.

but you can represent those interfaces using canonical structures instead.

all that applies to writing _one_ interface to categories. There might be reasons to write two interfaces but it doesn't seem worth it unless there's a specific reason...

The HB should be usuable for type classes too, and one can even combine TC and canonical structures; see the canonical structures for the working Coq user.

I would be interested in contributing to efforts to get a category theory library set up in mathcomp. What can I do to help?

I think @Cyril Cohen said that this is a more long-term goal and the current priority is to develop Hierarchy Builder to the point where category theory naturally fits into that framework. If this is the case, should I try to contribute to Hierarchy Builder?

Patrick Nicodemus said:

I would be interested in contributing to efforts to get a category theory library set up in mathcomp. What can I do to help?

I think Cyril Cohen said that this is a more long-term goal and the current priority is to develop Hierarchy Builder to the point where category theory naturally fits into that framework. If this is the case, should I try to contribute to Hierarchy Builder?

Hi @Patrick Nicodemus yes there is a long-term goal, and indeed it is based on Hierarchy Builder.

(cf https://github.com/math-comp/hierarchy-builder/blob/master/examples/cat/cat.v as a proof of concept)

We will have people working on it, and there is some setup to do before we can actually start, including adding universe polymorphism to HB...

I am afraid I have no visibility on the development of this library for now, but we will certainly need a lot of help to complete the library once we start. Maybe I can ping you when we are ready and we could also call for regular meetings for whoever wants to contribute then?

I'm interested.

I am interested in using it :sweat_smile: , I have seen many denotational semantics for MLTT described in categorical semantics, and it will be interesting to see how the formalization for those will look like, starred for future reference

general question, in principle, there is no problem automatizing a category theory powerful enough of describing coq in coq itself, right ? as long as it is based on axioms?

I am also interested.

Last updated: Jul 15 2024 at 20:02 UTC