I've recently started a development in MathComp of basic notions of modern (i.e., Grothendieck-style) algebraic geometry. My initial goal would be to define the notion of a scheme, and to do that I would first need to develop the notion of a sheaf. (BTW, I'm doing it in the classical way.) I'm using mathcomp-analysis for the classical set theory and topology and mathcomp-algebra for the basic ring theory part.

I wonder if there would be any interest from other MathComp users. As there are so many ways to do things (e.g., category theory), sometimes I wonder what is the "morally right" way to formalize notions like e.g. opposite categories.

Hi @Xuanrui Qi that's great. I guess categories should be formalized using packedclasses

Category theory has been done many times in Coq, but not in MC yet, I believe

https://coq.discourse.group/t/survey-of-category-theory-in-coq/371

Maybe it is the occasion for adding universe polymorphism to Elpi and Hierarchy Builder?

@Cyril Cohen That's indeed what I'm using now. I currently have a very basic hierarchy only (category -> productCategory; functor -> presheaf -> sheaf). But I want to define the notion of topos someday and that will indeed include a fairly complicated hierarchy.

@Xuanrui Qi as @Enrico Tassi mentions, it may be useful to build it using Hierachy Builder when we fully support universe polymorphism (do you have an idea how long it would take Enrico?)

I currently don't have any universe polymorphism now, but I would soon need it (e.g., to define the category Cat of Type-small categories, and the categories PSh and Sh)

Dunno, but without a use case the motivation is 0 ;-)

As @Xuanrui Qi said it might be necessary once you get to any category of some class of categories, (and one gets there really fast)

I haven't looked at this carefully enough, but is math-comp suitable for this?

E.g. choicetypes seem somewhat unnatural when working with universes.

I'm not at the stage of working with choiceTypes yet, but since I'm doing everything classically every type is a choiceType. I guess that simplifies part of the problem

hmm, I think one might differentiate between:

- category theory using packed classes, in any way possible
- category theory integrated with MathComp generally, following the MC encoding style and existing hierarchies

It seems to me 1. is possible/feasible, but like Bas I'm skeptical of 2., i.e., whether it's a good idea to hook into the existing MC hierarchies (after having looked at all the exotic encodings used in other Coq category theory libraries).

If you start from scratch (I mean, not plugging your structure into MC's hierarchy) then it would be really nice to try to use Hierarchy Builder for this, and would motivate me to add full support to universe polymorphism, which is today absent.

For those who may be interested, I have created a Element/Riot chatroom (https://matrix.to/#/!xRGtNQXoZBhMCllIEL:matrix.org?via=matrix.org) to discuss issues relating to developing category theory/topos theory/algebraic geometry in Coq/MathComp.

Interesting, but why yet another communication channel?

Indeed, I suggest we keep discussing it on the math-comp users stream on zulip, and if the conversation happens to span too many topics, we might open up a new dedicated stream. @Xuanrui Qi wdyt?

We can also keep it here. We (me and Reynald) already use Element for several other projects so it was convenient for us, but if others think otherwise we should keep it here.

The category theory part at: https://github.com/xuanruiqi/categories

Last updated: Jan 29 2023 at 19:02 UTC