redefine Bifunctor

[Alizter]

In this PR, we redefine Is0Bifunctor and Is1Bifunctor as discussed in #1933.

This has simplified things in lots of places however I got stuck with a universe issue in AbExt. @jdchristensen would you be able to take a look at that?

The reason I am doing this PR now is that I need some definitionally involutive opposite behaviour for bifunctors in #1929 and this isn't possible with the bifunctor coherence defintion.

[jdchristensen]

Overall it looks like there are some simplifications and some places that are a bit longer, but that overall things are simpler than before. And probably with another pass through it, you'll be able to remove some unneeded things, so it'll be even simpler.

[Alizter]

@jdchristensen I have some applications in mind for this. It has helped simplify the opposite of a monoidal category. I will work a bit more on that so that we can be sure this is worth it.

The reason I am interested in that is so that I can write down a cocommutative comonoid in a monoidal category which is just a commutative monoid in the opposite monoidal category.

[jdchristensen]

The approach to bifunctors in this PR causes some awkwardness that I'd like to discuss, and which showed up in SixTerm.v. ab_hom A B is the abelian group of group homomorphisms from A to B. It's a 0-functor in each variable in a natural way using pre- and post-composition. This makes it into a 0-bifunctor. However, when you then apply fmap10 to this bifunctor (using the set-up in this PR) along a map f : A -> A', you get the map sending g : A' -> B to Id $o g $o f, with an extra identity map involved. (We could instead use fmap (flip ab_hom B) f, but I couldn't get Coq to accept this in the context it comes up for some reason, even with various implicit arguments provided.) The same thing will happen for hom functors in general. And even for more general bifunctors, if we construct them by starting with a 0-functor in each variable, it would seem better if fmap10 and fmap01 returned the same definitions that we provided.

Couldn't we define the bifunctor class so that it remembers the functoriality in each variable and returns it when fmap10 and fmap01 are applied, and then have wrappers that provide constructors for how it is in this PR as well as accessor functors that provide the data used in this PR? I think this roughly describes how things are currently in master branch. It should be possible to use this set-up to make things as clean as they are in this PR, but retain the good behaviour of fmap10 and fmap01. In other words, I'm suggesting that if we go back to how things are in master, we should be able to find places where using the constructors/accessors I describe allow things to simplify like they do in this PR.

@Alizter said that he wanted this approach for other reasons related to opposite categories. Maybe those definitional equalities can still be achieved if things are done carefully? Or, if not, we have to think about whether it is worth having more complicated fmap10 and fmap01.

[Alizter]

Yes, this is an unfortunate side-effect and I am not happy with it. I will attempt to mix the two definitions and see if we can get the best of both worlds. This will mean I have to reintroduce the fmap01_is_fmap11 homotopies back as they would become data in the definition.

Something interesting I just realised is that this mixed definition is the one they use in Haskell: https://hackage.haskell.org/package/base-4.19.1.0/docs/Data-Bifunctor.html#t:Bifunctor but take that with a pinch of salt since they don't have 2-cells to worry about.

[jdchristensen]

I will attempt to mix the two definitions and see if we can get the best of both worlds.

This isn't what I meant above, but I was also thinking about it as an option. The class would have the fmap01, fmap10 and fmap11 data, plus a single(?) law saying that fmap11 can be expressed in terms of the other two. (The laws about expressing fmap10 and fmap01 in terms of fmap11 should follow, I think.) And in addition to the default constructor, there would be one taking just the fmap10 and fmap01 data and deriving fmap11. And there would be one taking just fmap11 and deriving fmap10 and fmap01 (using Is01Cat structures). Then depending on which constructor you used, some of the data you get back when using the instance would agree with what you put it.

That might work. But it might also work to just have the fmap01 and fmap10 data in the class, like in current master, and use wrappers for fmap11 and the fmap11 version of the constructor.

[Alizter]

I'm currently trying this out:

Class Is0Bifunctor {A B C : Type}
  `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C) := {
  is0functor_bifunctor_uncurried :: Is0Functor (uncurry F);
  is0functor01_bifunctor :: forall a, Is0Functor (F a);
  is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
}.

...

Class Is1Bifunctor {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F} := {

  is1functor_bifunctor_uncurried :: Is1Functor (uncurry F);
  is1functor01_bifunctor :: forall a, Is1Functor (F a);
  is1functor10_bifunctor :: forall b, Is1Functor (flip F b);

  fmap11_is_fmap01_fmap10 {a0 a1} (f : a0 $-> a1) {b0 b1} (g : b0 $-> b1)
    : fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0;
  fmap11_is_fmap10_fmap01 {a0 a1} (f : a0 $-> a1) {b0 b1} (g : b0 $-> b1)
    : fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g;
}.

It appears to be working well, but I haven't finished using it yet. The idea is that you have access to the finer functor actions so that you don't pollute terms, and there are always coherences taking you back to the other view.

[jdchristensen]

I'm currently trying this out:

That looks reasonable! It makes sense to have those two laws, not just one like I said. And I think many bifunctors naturally have efficient descriptions of all three functorialities, so they might just use the default constructors.

[mikeshulman]

I haven't looked at this particular case at all, but just wanted to point out that sometimes when there's more than one possible definition of something, it's useful to have both of them in a library, along with the equivalence between them. Then the more convenient definition can be used whenever a choice is possible, and we control when to go across the equivalence.

[Alizter]

I haven't looked at this particular case at all, but just wanted to point out that sometimes when there's more than one possible definition of something, it's useful to have both of them in a library, along with the equivalence between them. Then the more convenient definition can be used whenever a choice is possible, and we control when to go across the equivalence.

In this particular case we have two equivalent definitions that each have convenient behaviour in different places. We are looking into generalising both at the same time to have both sets of behaviours whilst still specialising to both definitions.

[mikeshulman]

Yes, my point was if it doesn't turn out to be possible to get both sets of behaviors at once, then a next-best solution might be to keep both definitions around and use whichever is convenient in different places.

[Alizter]

I've pushed the best-of-both-worlds definition and it builds. I haven't gone over the proofs in AbSES yet to make sure they are simpler.

[Alizter]

It seems to have worked. Overall many things got renamed, but there is a clear advantage in the join formalization. IINM this should allow us to use the twist construction directly there.

[jdchristensen]

I'm not quite done my review, but will continue later. I'm also about to push some simplifications.

[jdchristensen]

Maybe we should swap the direction of bifunctor_coh so that these two lines become exact bifunctor_coh or even exact _?

[Alizter]

I tried this, but IIRC I had to switch direction in other places as well.

[Alizter]

Alternatively, we could split the assumption into two.

[jdchristensen]

Alternatively, we could split the assumption into two.

Not sure what you mean by this. But another alternative is to change the definition of Is0Bifunctor'' to be the other choice. But then probably lots of other things would change, and there's little benefit.

[Alizter]

I guess I wasn't thinking straight earlier. I was thinking of the fun11_is_fun01_fun10 coherences but they don't make sense in this context.

[jdchristensen]

I wonder if other places that use fmap01 and fmap10 for this bifunctor would get simpler if we used Build_Is0Bifunctor and provided the more direct functoriality in each variable as well?

[Alizter]

One thing I would like to use this in is the twist construction for the smash product. I was thinking before that we would run into the awkwardness that join did and that it would be less manageable since the smash is tricky to work with. Now however I think everything is in place to prove the associativity of smash. We just need to construct the twist map.

[jdchristensen]

Maybe this bullet is also a lemma that can be put into Prod.v?

[Alizter]

This doesn't fall into that category since it is specifically about the instances built in Build_Is0Bifunctor''. If you unfold the proof here you will see that it isn't the usual uncurry instance but rather one where it is built from the fmap in each parameter.

[Alizter]

I may have misunderstood what you meant however.

[jdchristensen]

I'll show what I meant in a fresh PR.

[jdchristensen]

I've now finished reviewing, and think it looks good. There are still a few comments that could maybe be addressed, but it's ok if they don't work out.

[Alizter]

I will merge once the CI is green.