Trick to make Is1Cat definitionally involutive

[jdchristensen]

I was curious how close is1cat_op is to being definitionally involutive, and it turns out that the only thing that fails is associativity, because it requires using gpd_rev on the hom types.

We could consider making a variant of Is1Cat without associativity and using that where possible, to avoid duplicating dual proofs. But it would add one more layer in the WildCat hierarchy, so I don't think it's a great idea.

Instead, the second commit shows a trick that makes this work. It changes Is1Cat to have two associativity proofs, one for each direction, with is1cat_op' just switching the two. We could define Build_Is1Cat to only take one, and prove the other using gpd_rev, so almost no code would need to change. (And we already define cat_assoc_opp, so this is really no different from what we've got, except that it gets moved into the data of Is1Cat.)

In this PR, this is all done in test/WildCat/Opposite.v, but if it looks like a reasonable change, then I could make it to the main code. Then several other places with dual proofs would simplify.

[jdchristensen]

Hmm, this might not work like it is, since we probably use in some places that cat_assoc_opp is the inverse to cat_assoc. If so, we would need to add that (and its dual) to Is1Cat. Or maybe this would only come up with 2-categories?

[Alizter]

I guess you are right that this would only apply for (2,1)-cats. We could simply add some extra coherence stating that cat_assoc_opp is left and right inverse to cat_assoc. That way cat_assoc would be a natural equivalence in another way.

[jdchristensen]

I just pushed four commits.

The first one moves this trick from the tests/ folder and makes it our real definition of Is1Cat. In order to make things smooth, I had to also add the reverse associativity in other places, e.g. in Is1Cat_Strong and IsD1Cat (displayed).

Second commit: I also found a way to make core and op commute definitionally, by making some proofs more symmetric.

Third: is1functor_op' now simplifies.

Fourth: speed up a few things. Now the speed is unchanged within the noise.

Note: I didn't need to use anywhere that the two proofs of associativity are inverse to each other.

Question: Is the mild increase in complexity worth it? I'm inclined to think so.

Question: Can other things simplify now that is1cat_op is definitionally involutive? There's a spot in #1929. Anywhere else?

[Alizter]

Question: Is the mild increase in complexity worth it? I'm inclined to think so.

Yes, I agree. This isn't the only structure we have in the library with "redundant" data. I believe bundled equivalences and groups also fall into this category. I think the gain of a definitionally involutive op will be well worth it.

Question: Can other things simplify now that is1cat_op is definitionally involutive? There's a spot in #1929. Anywhere else?

I would check the binary coproduct functoriality proofs. IIUC these should follow definitionally now.

[jdchristensen]

I would check the binary coproduct functoriality proofs. IIUC these should follow definitionally now.

They use is0functor_op and related things, which are just the identity function, but with types that make things work smoothly. So I think that by fixing is1functor_op', I've handled this. But I didn't look through that file. Let me know if there is something you see there.

[Alizter]

Nice! I had a look at coproducts but didn't spot any obvious simplifications.