Bifunctors

[gio256]

A number of updates to WildCat/Bifunctor.v have been discussed in #1878. This is a tracking issue for changes that don't make it into that PR.

TODOs include:

• Renaming (in particular, IsBifunctor -> Is0Bifunctor)
• A consistent plan for working with curried and uncurried bifunctors and moving between the two. Currently, the PR above introduces some lemmas for uncurried bifunctors that don't mesh very well with the rest of the work on curried bifunctors. These should be renamed and either moved to WildCat/Prod.v or made to fit better with the other lemmas in WildCat/Bifunctor.v.
• Should the bifunctor coherence condition (bifunctor_isbifunctor) be moved into Is1Bifunctor, leaving Is0Bifunctor with just Is0Functor instances in each argument? This seems to be more consistent with the unbundled structure of functors. Also, in order to prove that an uncurried bifunctor is a curried bifunctor, I needed Is1Functor to prove Is0Bifunctor. My hope would be that moving the coherence condition into Is1Bifunctor would limit the extra assumptions needed to move between the curried and uncurried forms.

[Alizter]

We had discussions about the name Bifunctor previously. I think Mike mentioned that he doesn't like the name since it conflicts with bifunctors from bicategoires which is common in the 2-category literature. These are also called weak 2-functors and peudofunctors (in special cases) but the bifunctor terminology fo 2-ary functors is very common in homological algebra literature.

Since we've named binary products BinProducts rather than Biproducts which is something that is a product and a coproduct (and something we will need to have soon), we could consider doing the same for functors and calling them BinFunctors rather than Bifunctors.

On the other hand, we don't really do any wild bicategory theory, nor do I see a reason to do it just yet (as almost all of our examples are wild (2,1)-categories). So maybe it is not as ambiguous as seems currently.

[jdchristensen]

@Alizter That's an orthogonal naming issue. I'm talking about how both F : A -> B -> C and F : A * B -> C are called "bifunctors". In PR #1886 they are called "uncurried bifunctors" or "bifunctor_uncurried" in identifiers, which helps a bit to distinguish them. This is probably good enough, since we don't seem to have great choices for alternate names.

[Alizter]

What if we call F : A -> B -> C a bifunctor and F : A * B -> C a functor? Wouldn't that reduce the redundancy?

[jdchristensen]

Taking this as a concrete example:

Global Instance is1bifunctor_bifunctor_uncurried {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
  : Is1Bifunctor (fun a b => F (a, b)).

we would change the name to is1bifunctor_functor_uncurried. That's also fine to me. In prose, we could change things like

(** *** Uncurried bifunctors are functorial in each argument. *)

to

(** *** A functor on a product category is functorial in each argument. *)

I'm ok either way.

[Alizter]

I think the second one reads better. We should also say "from a product category" as "on" is a bit ambiguous.

[Alizter]

So after some thinking, I've come to the conclusion that it might be better to define bifunctors using uncurry and having the coherence based definition as a "smart constructor". My reasoning is as follows:

In many cases of functoriality, we can prove things in both variables simultaneously. Take for instance the smash functor I defined in #1892. There, the uncurried version of the bifunctor would have a more compact term. In that PR, I defined the functorial action of Smash simultaneously and then specialised to each variable and then proved that it was coherent. It seems like it would be less work and less space to define the unurried functor directly.

The definition in most classical literature that I have seen define a bifunctor as the uncurried version and as a lemma it is shown to be equivalent to the component-wise data and coherence condition.

Overall I think it would be best to redefine bifunctor as functoriality of the curried version and have a smart constructor for building them with the current definition's data and also derive the functoriality in a single variable.

This way also has the advantage that it scales better with respect to the number of variables, but we hardly ever need a notion of trifunctor. (Or maybe it would be useful for TriJoin?)

FTR the definition I have in mind is:

Class Is0BiFunctor {A B C} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) := {
  is0functor_uncurry_bifunctor :: Is0Functor (uncurry F) ;
}.

[jdchristensen]

I've come to the conclusion that it might be better to define bifunctors using uncurry

That might make sense. The same thing happened with is1bifunctor_join, for example, in #1886. It we go this route, does it still make sense to use F : A -> B -> C, or should we just use F : A * B -> C? I guess most of the examples come naturally in the first form.

[Alizter]

@jdchristensen Yes F : A -> B -> C, otherwise we wouldn't really need a notion of bifunctor.

[gio256]

Would it be helpful if I went through and repeated the proofs of e.g. is1bifunctor_join in #1886 using the lemmas below for comparison?

Definition Build_Is0Bifunctor' {A B C : Type} `{Is01Cat A, Is01Cat B, IsGraph C}
  (F : A -> B -> C) `{!Is0Functor (uncurry F)}
  : Is0Bifunctor F
  := is0bifunctor_bifunctor_uncurried (uncurry F).

Definition Build_Is1Bifunctor' {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
  : Is1Bifunctor F
  := is1bifunctor_bifunctor_uncurried (uncurry F).

I think either way around works well, though my guess would be that the current definition ends up being slightly easier to use while being slightly harder to define directly. It might just be me, but unification seems to struggle at times when product categories are involved.

[jdchristensen]

It does seem like @gio256 's approach also gives us the same simplifications that we would get if we changed the definition of Bifunctor. So maybe it is a better way to go? I do slightly prefer the current definition of Bifunctor as it doesn't involve product categories directly.

[Alizter]

The only difference is that the uncurried version will be more compact. Since it is more work to unpack an uncurried functor and pack it up again. There will be quite a large term size if we continue this way. The bifunctor data we have now is convenient, but I don't think it will be the most common form. I suppose for Ext, it makes sense, but when you consider other bifunctors you can see that choosing the one I suggested will keep all the term sizes smaller overall.

In any case, it won't make any difference in the proofs if we start using the lemmas that @gio256 suggested as it can easily be changed. Only when we reason about the functors themselves will we notice that terms are larger than we would expect.

[Alizter]

I suppose it's fine to continue the direction in #1886 once we start using the lemmas @gio256 suggested. We can keep this issue open afterwards and experiment with swapping out the definition in another PR.

[Alizter]

I think that this issue is complete. I'll create another issue about experimenting with redefining bifunctor. I don't want to touch it right now because we are building a lot on it at the moment.