Stream: math-comp users

Topic: Category Theory

Patrick Nicodemus (May 23 2022 at 05:46):

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.

1. 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)
2. I want my own work to be more useful to others because it is submitted in the context of an existing library.
3. I would like the code review and helpul feedback which comes with submitting to a library

Patrick Nicodemus (May 23 2022 at 05:47):

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

Bas Spitters (May 23 2022 at 10:39):

We're combining cat th with math comp in our SSProve library:
https://github.com/SSProve/ssprove/tree/main/theories/Relational

Cyril Cohen (May 25 2022 at 12:02):

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

Patrick Nicodemus (May 26 2022 at 22:49):

Thanks @Cyril Cohen , looks really interesting!

Patrick Nicodemus (May 28 2022 at 06:33):

@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?

Ali Caglayan (May 28 2022 at 22:12):

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

Ali Caglayan (May 28 2022 at 22:15):

"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.

Paolo Giarrusso (May 28 2022 at 22:16):

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

Ali Caglayan (May 28 2022 at 22:18):

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

Ali Caglayan (May 28 2022 at 22:18):

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

Julien Puydt (May 30 2022 at 05:20):

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.

Cyril Cohen (May 30 2022 at 11:14):

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 ltone would end up generating a too strong definition of homomorphism (so one should be able to explicitly omit lt in the instance)

Patrick Nicodemus (May 30 2022 at 13:07):

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?

Patrick Nicodemus (May 30 2022 at 13:07):

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

Paolo Giarrusso (May 30 2022 at 13:26):

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.

Paolo Giarrusso (May 30 2022 at 13:27):

but you can represent those interfaces using canonical structures instead.

Paolo Giarrusso (May 30 2022 at 13:30):

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...

Bas Spitters (Jun 06 2022 at 14:25):

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.

Patrick Nicodemus (May 21 2023 at 20:01):

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?

Cyril Cohen (May 21 2023 at 20:14):

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?

Ricardo (May 21 2023 at 23:39):

I'm interested.

walker (May 22 2023 at 12:20):

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

walker (May 22 2023 at 12:24):

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?

Ali Caglayan (May 23 2023 at 15:39):

I am also interested.

Last updated: Oct 13 2024 at 01:02 UTC