Bundled categories

[patrick-nicodemus]

Introduces a bundled type of Graphs and a bundled type of Categories.
Proves that Graph is a (0,1)-category and a 2-graph.
Proves that Category is a (0,1)-category and a 3-graph with "wild modifications" as 3-cells.

[Alizter]

Quick comments:

If you want to do "module driven development" (a la OCaml), typically its better to write t, so the type becomes Graph.t. Also you can do Export after the module for the instances and coercions using import/export filters.

However, we typically avoid uses of modules in the library, as it can make understanding things a lot harder. Coq's module system also differs from OCaml's module system in some painful ways which makes using them a lot less ergonomic.

Here the goal is to introduce a namespace. I would instead prefer that the bundled Graph lives in its own file in WildCat/Graph.v. The name of the type should be Graph and the fields should be graph_carrier and isgraph_graph_carrier.

[patrick-nicodemus]

I think that there will be a necessity to later bundle other structures as well for similar reasons as to here, so I wanted to do this in a prudent way. I know that the math-comp library has used this style of "packed classes" which is organized around the module system, so I looked in the book "Mathematical Components" textbook by Mahboubi and Tassi https://math-comp.github.io/mcb/, Section 8.3 describes this style. I am not experienced enough with tall hierarchies to have a feel for why this style is important but I thought of it as a kind of "defensive" approach.

If you want to do "module driven development" (a la OCaml), typically its better to write t, so the type becomes Graph.t.

I am familiar with this OCaml convention. The name type appears to be the math-comp convention, from the book cited.

we typically avoid uses of modules in the library, as it can make understanding things a lot harder. Coq's module system also differs from OCaml's module system in some painful ways which makes using them a lot less ergonomic.

Can you elaborate on this? I think moving things to their own file in Graph.v and Category.v is fine but I am wondering about what the pitfalls are with the use of modules (both difficulty of understanding and inconvenience). You can link to previous discussions or Zulip threads.

[Alizter]

My main gripe with Coq modules is that they are difficult for newcomers to understand. Have everything laid out flatly can greatly benefit readability, and I am not yet convinced modules buy us any advantage when it comes to "modular code generation".

A classic example of the pitfall of modules is the Coq stdlib material on natural numbers and integers. All such lemmas are sparsely populated between many different files, and some definitions are generated with module functor applications. Implementations of these definitions become difficult to source or follow, which makes proving properties about them all the more difficult.

The library has always been hesitant to use modules in the past and we had one big use that was difficult to work with. There were various universe bugs that stopped us from having a good definition of modality a few years ago. Because of this there was some module magic whose sole purpose was to share the work between reflective subuniverses and modalities. It made understanding the code very difficult, which wasn't helped by Coq's lack of good documentation at the time. Eventually, it was fixed so that a modality was a special case of a reflective subuniverse, and this made working with it easier. That's one example from memory.

[Alizter]

Why have this separate? It should be the fields of the type.

[patrick-nicodemus]

I can collapse Category.type and Category.class_of into one layer if you want, I am just trying to follow the packed-classes discipline as closely as possible.

[patrick-nicodemus]

I have collapsed this in the current PR to get things to go forward but I think we should discuss some bundling methodology or standard approach to use. As I said before, bundled versions of structures will often be necessary so there has to be some style to use, it will be nice to have a discussion about the kinds of issues that may arise with different styles.

[Alizter]

Yes, we should definitely discuss some of the tradeoffs. When I last looked into this problem, it wasn't obvious which solution would be better.

[patrick-nicodemus]

@Alizter While following up on your comments, I noticed that there is already defined a type of bundled Graphs in Diagrams.Graph. I was not aware of this, and I assume we should not duplicate it? I imagine it is it better to have Diagrams refactored to depend on WildCat.Graph, but this will take some work and so perhaps we should discuss what reorganization is appropriate before I dive into it.

(This can also be deferred to a later PR, if we want to limit the scope of this PR.)

[patrick-nicodemus]

@Alizter I made the changes you suggested. I tried to match the indentation and line break style to other code in the WildCat library but it's not super consistent through the library.

[Alizter]

Actually, I have a few minor changes. If you are alright with it, I can push directly here and save some back-and-forth.

[patrick-nicodemus]

Yes that sounds good

[Alizter]

It might be interesting to replace Diagrams.Graph now that we have this. I don't think we should touch that just yet however, as others are working on colimits at the moment so we don't want to give them a hard time rebasing.

[jdchristensen]

BTW, is there any overlap with things in ZeroGroupoid.v? Or at least, are the styles compatible?

[Alizter]

I am the one to blame about the comments. I wrote them a bit too quickly my bad. Feel free to fix, I will check them again later today.

[patrick-nicodemus]

I was not familiar with the ZeroGroupoid file before you pointed it out. They are written in the same style so it's consistent. On the other hand some things are deliberately redundant in that file. I created a post in the Coq Zulip to get feedback on whether it would be appropriate to relate bundled Graphs to bundled ZeroGroupoids more directly

[patrick-nicodemus]

I just added a second commit in response to @jdchristensen 's question about whether ZeroGroupoid should be refactored to depend on Graph. We can use the isgraph_induced, is01cat_induced and is2graph_induced to show that these structures on ZeroGroupoid are inherited from the type Graph. However, the author of the ZeroGroupoid file deliberately duplicated an isomorphic copy of the Fun01 type because "we put a different graph and 01-category structure on it, so we give this a custom name", so they might have good reasons for not wanting this functionality to be merged. (The fix was easy, just a lot of renaming.)

[jdchristensen]

I wrote the ZeroGroupoid.v file, and I guess I thought that Coq would get confused if Fun01 had more than one graph (etc) structure. But since these instances come from the underlying type of objects rather than the type of morphisms, I guess there is no confusion. So these latest changes look good to me.

[jdchristensen]

The overall PR looks good to me.

One procedural comment is that I would reduce the use of forced pushes. They are appropriate in some cases, e.g. to remove a commit that we decide should be omitted, but in general it's easier to follow the progress in a PR when fixes are pushed as new commits. If by the end there are too many such minor fixes, some of the commits can be squashed before merging.

[patrick-nicodemus]

But since these instances come from the underlying type of objects rather than the type of morphisms, I guess there is no confusion.

I've been a little worried about what will happen here if unification applies coercions to some of the objects involved. For example given Category objects C, D, F, G : C $-> D and tau : F $-> G, we might (for whatever reason) use C and D in a term in such a way that Coq thinks it has to coerce them to something weaker such as a Graph, and then F and G are inferred to be graph homomorphisms and tau is inferred to be a wild natural transformation. In this example that did not see a problem but while debugging a breakage in unrelated work I noticed that in a theorem about Abelian groups, when you did Set Printing All, coercions to Group had been applied basically everywhere even though it was clear to me from context that the analogous AbelianGroup structures were supposed to be used without any coercions being inserted. (That's not as serious as tau being downgraded from a natural transformation to just a transformation, because you don't really lose any strength)

[patrick-nicodemus]

The overall PR looks good to me.

One procedural comment is that I would reduce the use of forced pushes. They are appropriate in some cases, e.g. to remove a commit that we decide should be omitted, but in general it's easier to follow the progress in a PR when fixes are pushed as new commits. If by the end there are too many such minor fixes, some of the commits can be squashed before merging.

Definitely! Understood.

[jdchristensen]

Your last point is a good one, and I'm not sure how to deal with it, except to use more (A:=...) annotations.

[jdchristensen]

@Alizter Do you want to review this? Modulo my one comment request, I think this is ready to merge.

[Alizter]

Modulo my comments, this LGTM.

[patrick-nicodemus]

Both comments have been addressed