Stream: math-comp users

Topic: Category Theory


view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (May 23 2022 at 05:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (May 26 2022 at 22:49):

Thanks @Cyril Cohen , looks really interesting!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (May 28 2022 at 22:16):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (May 30 2022 at 13:27):

but you can represent those interfaces using canonical structures instead.

view this post on Zulip 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...

view this post on Zulip 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.


Last updated: Jan 29 2023 at 19:02 UTC