Displayed Wild Categories

[gio256]

This is a refresh of work by @emilyriehl and others that can be found here. The ultimate direction is still unclear, so any thoughts to that effect are appreciated.

A few arbitrary conventions that are up for debate:

• Where possible, anything that exists in WildCat/Core retains the same name prefixed appropriately by d (or D). For example, Is1DCat and dcat_comp.
• A single tick indicates that an object or structure lives in a displayed category over the underlying object or structure. For example, if a : A then a' : D a, and composition in displayed categories is denoted g' $o' f' over g $o f.

[jdchristensen]

Thanks for this, @gio256! It looks like we should review all of these commits at once, right? I think it would probably be good to squash these before merge, since they contain rough work along the way, but we can worry about that after review.

Can you summarize how this is different from the file Displayed.v in the tree you linked to?

[jdchristensen]

@gio256 The title says "WIP": can you say what you think still needs to be done?

[jdchristensen]

I only skimmed the rest for now, but didn't notice any other issues (besides the ones below). The proofs seem to nicely follow our style.

[gio256]

Can you summarize how this is different from the file Displayed.v in the tree you linked to?

This is basically the minimum necessary changes to get that file working again and caught up to the current state of Core.v.

There are still a few sections of Emily's branch that aren't included here, namely functor composition and products of displayed categories. I think completing those and then revisiting makes sense.

[emilyriehl]

Thanks @gio256 and @jdchristensen for your careful attention to this. As I think was discussed on the Zulip, this was done ages ago when @mikeshulman invited several novice Coq users for a week-long workshop to try to make some useful contributions to the WildCats library. But despite the best efforts of our hosts/coaches, it's likely that the code in here is inelegant and buggy so please feel free to make any improvements you see fit.

[jdchristensen]

This is looking great. Thanks for the quick fixes. @gio256, is there still more you'd like to do?

[gio256]

I think it is at feature parity with the original branch and ready for review. The big thing still on my mind is making sure that all the typeclass constraints are as minimal as possible.

[jdchristensen]

@gio256 Is it ok if I push a commit or two to your branch?

[jdchristensen]

Ok, I pushed three commits. @gio256, please check them over. I'm not an expert on the backtick and ! syntax for typeclasses, but I found a few places where I could simplify them without duplicating superclasses. The second commit uses snrapply instead of srapply in three places for speed. (It's on the order of 0.04s per change, so very small, but 25 such lines add up to 1s.) And the last commit avoids destructing various pairs, which should result in a smaller proof term.

@Alizter, do you have any comments, or is this good to go?

[jdchristensen]

BTW, before merge, I'd be inclined to squash the first 18 commits into 1, but leave the rest to reflect changes made during review. @gio256, we normally don't squash, so when we make a PR, we try to have the commits reflect logical steps for review.

[mikeshulman]

Thanks for doing this! I'm very happy to see this work rescued from oblivion.

[gio256]

Thanks @jdchristensen for the changes.

I'm happy to squash (or have squashed) any combination of commits, but I'm not sure I fully understand the convention. Is there something I should do here that is preferable to just squash merging the branch?

[jdchristensen]

I'm happy to squash (or have squashed) any combination of commits, but I'm not sure I fully understand the convention. Is there something I should do here that is preferable to just squash merging the branch?

Our githib repo is configured to not allow squash merges, because we normally like to see the history, and squash merges also don't play well with work that builds upon them. Instead, we try to make PRs that have commits that we would want to see in the history. In this case, once Ali confirms this is good, I can use git to squash the first 18 commits, and then force push to here before merging.

BTW, do you have plans to make additional PRs? Do you have a particular direction you are interested in pursuing?

[jdchristensen]

One thought for future work:

1. Make lemmas named something like isgraph_equiv_isgraph that say that if we have A <~> B and IsGraph A, then we get IsGraph B. Same for the other Wildcat typeclasses.

2. Then we can use this PR to create wild category structures on various sigma types, and then use issig and the lemmas from 1) to transfer these to wild category structures on records.

3. See if this simplifies the construction of any of the wild categories we have, e.g. pType, Group.

4. Can we make some tactics (edit: or, even better, lemmas) that can handle step 2) in a semi-automatic way? E.g., I specify the type family (possibly assumed to be over Type), and the tactic creates a displayed category structure with natural choices for the morphisms, etc. Or maybe I have to specify something with a bit more structure, e.g. a monad.

[Alizter]

I've left some comments.

[Alizter]

I've left some comments but I'm happy with going forward with this.

[jdchristensen]

@gio256 You can hit the "Resolved" button as you address things, so it's clear what remains. I'll look at this again tomorrow.

[jdchristensen]

1. Make lemmas named something like isgraph_equiv_isgraph that say that if we have A <~> B and IsGraph A, then we get IsGraph B. Same for the other Wildcat typeclasses.

This is already done in WildCat/Induced.v, and just needs a map (in the other direction), not an equivalence.