Update bifunctors

[gio256]

Depends on #1878. Addresses main points in #1883, except for changing the definition.

The big change is moving the bifunctor coherence condition to Is1Bifunctor. Unfortunately, this means that for any previous proofs of Is0Bifunctor we either need 1-functoriality to prove Is1Bifunctor, or we throw away the coherence proof. As far as I can tell this has been without incident so far.

[Alizter]

I will take a look after #1878.

[jdchristensen]

This looks good! My only other comment is that there are a few places where the proof of the coherence condition has been removed. Would it be hard to prove Is1Bifunctor in those cases so we still have that information? Or at least to state the coherence as a separate lemma, which could in the future be merged into a proof of Is1Bifunctor?

[gio256]

There are a few places where the proof of the coherence condition has been removed.

So far I have only taken the low hanging fruit here, and I haven't looked closely enough to know if there are any instances where we won't be able to prove Is1Bifunctor (maybe with an extra assumption). I like the idea of including the coherence as a separate lemma so it's not just lost.

Would it be worth adding an extra class IsCoherentBifunctor that includes the coherence separately from Is1Bifunctor?

I don't know that there are any lemmas that could be proven from Is0Bifunctor, !IsCoherentBifunctor other than the agreement of the two routes to Is0Functor (uncurry F), but maybe there are still interesting cases where that helps.

[jdchristensen]

Would it be worth adding an extra class IsCoherentBifunctor that includes the coherence separately from Is1Bifunctor?

I would first try to see if we can just prove Is1Bifunctor in all cases, rather than create a third Class.

[Alizter]

I just wanted to quickly add that it seems that the definition of bifunctor with the coherence condition is the correct one. See for example http://www.tac.mta.ca/tac/volumes/37/34/37-34.pdf where the authors work this out for pseudofunctors (which our functors a special case of).

I'll think some more today and see if I can sketch a counterexample for something that is functorial in two arguments but not in both. This appears to be related to the Gray tensor product.

With regards to library organization, I don't think we have any examples of bifunctors which don't have this coherence condition, so keeping it all packaged up should be good.

[Alizter]

@gio256 I updated the description of the PR to no longer close #1883 so that we can think about changing the definition in another PR. I think its fine to continue this direction, using the uncurried helpers for Join etc.

[jdchristensen]

Having to introduce various "buildequiv" constructions is a little annoying. One thing that would help would be to use pose or set to put these in the context. This also has the advantage of a smaller proof term, since they will be shared. This applies to other parts of the recent changes as well.

[gio256]

I'm having trouble figuring out what exactly to pose in this case. Maybe I'm misinterpreting your suggestion, but I haven't been able to make things cleaner using pose here so far.

I also have a tangential question: when we talk about wanting smaller proof terms, is the goal more readable terms, terms that are easier for coq to handle, or both?

[jdchristensen]

For example, you can add pose (feq' := Build_DCatEquiv f' (fe':=fe')). at the start of the proof, since that term is used twice in the proof. Same for other repeated terms.

In this case, it makes the tactic script easier to read, and also should produce a proof term that is easier for Coq to handle.

[gio256]

Oh I see. I think my confusion was really around the second question in this case, so thank you for clarifying.

[jdchristensen]

If you look at Coq's proof term when the pose command is used, it starts with let feq' := Build_DCatEquiv f' in ..., which shows that this has been factored out. It turns out that feq' appears 40 more times in the proof term (with implicit arguments shown), so this is a non-trivial savings. (BTW, this proof term is around 4000 lines long!)

[gio256]

Interesting. It's very unintuitive to me that this would improve coq's performance, so I greatly appreciate the suggestions.

[gio256]

This comment and the one below also raise two thorny issues with displayed categories I'd like to improve on:

1. Unification and typeclass search are clearly hindered (e.g. we need exact isd0gpd. everywhere). I would imagine there are more tricks like the above that can be used to help coq along here.
2. Every change to WildCat/Core.v or WildCat/Equiv.v now needs to be reflected in WildCat/Displayed.v or WildCat/DisplayedEquiv.v, respectively.

[jdchristensen]

I'm just skimming this, but I'm seeing lots of proofs getting longer. Can you explain in general what the latest changes are doing?

[gio256]

The idea was to introduce compose_catie' (dcompose_catie'), which is a variant of compose_catie that I think will make it slightly easier to prove when a specific map is an equivalence. The proof is the same, but slightly longer because we need to insert all the Build_CatEquiv terms.

This makes compose_catie a one-liner, but it also made the proof of cate_inv_compose longer as now there are two Build_CatEquiv terms to deal with there. Because of this, dcate_inv_compose also had to get longer.

I thought compose_catie' would be useful in the future (as well as for proving Bifunctor.iemap11), but if it's not strictly better we should revert it. I have also needed it before e.g. to prove that 2-of-6 holds for equivalences.

[jdchristensen]

I don't see why factoring compose_catie' out of compose_catie should make subsequent things harder to prove. I suspect that if you prove compose_catie' nicely, it should reduce to the same proof of compose_catie that you had before. But maybe the issue is that if you start with an equivalence, and then build a new equivalence with the same underlying map and same proof that it is an equivalence, you don't get back the equivalence you had? Unfortunately, I'm very busy for the next few days, so I won't have time to look into this, but I encourage you to see if there is a way to make this work out more simply. One obvious alternative is to revert to the old proof of compose_catie, and then define compose_catie' using it, instead of the other way around.

[gio256]

I will have a look. I suppose I wasn't sure which way around was preferable, but I think it's all resolvable with something like a cate_homotopic lemma.

[gio256]

I have used cate_homotopic to redefine compose_catie' in terms of compose_catie as you suggested. It would also be straightforward to remove one or both of these definitions if it's just simpler to avoid touching equivalences in this PR.

[jdchristensen]

Thanks, that looks reasonable. I thought about this a bit more, and my first intuition was that your previous approach would be better, since normally we first prove IsEquiv and then use that to prove Equiv. But with wild categories, it's trickier, since just from the CatIsEquiv type, you don't have access to any data, such as the inverse. You first have to build the element of CatEquiv, and even then, that gives you a retraction and section for a potentially different map (which is homotopic to the one you started with, but not definitionally equal). So this makes working with CatIsEquiv assumptions awkward. We could (1) throw up our hands and avoid making CatIsEquiv assumptions, instead having CatEquiv assumptions. (2) Add some lemmas that given a map f and a proof of CatIsEquiv f, return the inverse g and the proofs that f itself is a section and a retraction of g. (This is an idiom that you are using in a few places.) (3) Think hard about the definition of HasEquivs and see if there is a way to make this work better. There's a lot of redundancy in HasEquivs, and it's there to try to accommodate different settings, so it might not be possible to do better.

[gio256]

Is (2) something worth a small refactor to make CatIsEquiv assumptions a better default? I guess maybe best to spend some time on (3) first.

Do you know if anyone has tried to factor CatEquiv out of HasEquivs? I'm thinking of whether it's possible to provide the simplicity of a $<~> b without directly including it in HasEquivs.

[jdchristensen]

(3) is definitely something that would take some thought and experimenting, not as part of this PR. I don't know what people have tried. Some "obvious" things, like just getting rid of CatEquiv as data, and instead defining it to be { e : a $-> b & CatIsEquiv e } won't work because we want to be able to use wild categories is situations where there is already an existing notion of equivalence. I'm not sure if that's what you meant by factoring CatEquiv out of HasEquivs`. If you have another idea, please share it.

In the meantime, something like (2) could be part of this PR, since I think it would just mean taking a few repeated idioms and factor them out into lemmas. But it could also be left as something to think about later, and this PR could stay like it is.

[gio256]

I am happy with leaving this to think on and potentially include in a separate PR for now (assuming others feel the same).

[Alizter]

Could you also prove the 0gpd versions which appear further down? Those won't require MorphismExtensionality IIUC.

[gio256]

What do you think about proving is?functor_opyon using the bifunctor instances instead of the explicit proof that is there now? It seems like a repeated proof, but maybe an instructive one.

[Alizter]

I'm not certain. I think for now lets keep it repeated and merge it at another point if we think it would be slicker.

[Alizter]

Maybe @jdchristensen will have an opinion when he is available.

[jdchristensen]

I don't know exactly what is being discussed, but I'm all in favour of reusing proofs instead of repeating them (if it works smoothly).

[gio256]

I tried proving is?functor_opyon using the bifunctor instances, but it leads to a proliferation of extra identity maps in inconvenient places. I will play with it some more, but there might be a reason these weren't proven from the is?functor_hom instances previously, in which case maybe best just to leave a comment explaining why it is proven explicitly.

[gio256]

I have added a comment for this now, though I debated leaving no comment instead. It's a bit misleading, because there are really a number of reasons that we prove is0functor_opyon explicitly:

1. The reason stated in the comment, that using the bifunctor instance leads to extra identity maps in certain places.
2. It's an important functor, and it's instructive to prove explicitly and useful to control the resulting terms precisely.
3. It makes it easier to prove is0functor_yon as is0functor_opyon (A:=A^op), which is consistent with how the rest of the contravariant lemmas are proven.
4. That's the way it is now, and changing it breaks things

[Alizter]

This looks good to me. I've left a comment about the 0gpd version of the yoneda functor that would also be good to have.

[Alizter]

@gio256 Is there anything left to do here? I'm happy with merging as soon as @jdchristensen is too.

[gio256]

@Alizter I'm happy with the current state here. A few dangling questions above, but assuming everyone agrees that those can be considered resolved I think it's ready to merge.

[jdchristensen]

Thanks for all of the hard work on this!