Redundancy in definition of `Is0Bifunctor` is problematic

[patrick-nicodemus]

Coq-HoTT/theories/WildCat/Bifunctor.v

Line 10 in 5c605d7

(** We choose to store redundant information in the class, so that depending on how an instance is constructed, we will get the expected implementations of [fmap10], [fmap01] and [fmap11]. *)

The definition of Is0Bifunctor is deliberately redundant. But this means that if you assume a bifunctor structure on F, you actually are assuming two incompatible functor structures, and this led me to some hard-to-debug unification issues today where I couldn't understand why on earth these two terms weren't equivalent. For concrete instances of Is0Bifunctor I would expect that fmap01 a f and fmap (Id a) f are usually definitionally equivalent, but I really got bit today forgetting that they aren't definitionally equivalent (or propositionally equivalent, or equivalent up to a wild 2-cell) for a hypothetical instance of Is0Bifunctor. I see from looking through the Bifunctor.v file that if you assume that F : A->B->C is a 1Bifunctor and not just a 0-bifunctor then you have coherence 2-cells connecting these (fmap01_is_fmap11 and fmap10_is_fmap11) but are there important applications where fmap11 (Id a) f is not definitionally equal to fmap01 a f?

It should be possible to define fmap01 and fmap10 in terms of fmap11 if both A, B are 01-cats. If A, B aren't 01-cats it's not clear what fmap01 and fmap10 are supposed to be.

I think I would prefer if Is0Bifunctor was defined only in terms of fmap11 and then the functions fmap01 and fmap10 were defined as fmap (Id a) g or fmap f (Id b) in the case where A or B is a 01Cat respectively.

[Alizter]

I would assume functoriality in both arguments separately like we do for composition in the definition of a 1-cat. Bifunctoriality in our sense would be a "theorem".

We put a lot of effort into this definition of bifunctor to make it ergonomic. The proposal you give was tried but it leaves a lot of identity compositions sprinkled about. Here is the PR where we designed it if you want to get some more insight #1952

[patrick-nicodemus]

Okay, that's a good example of something where the two arguments need not be definitionally equal. I'll close the pr for now and reopen it if I can't find a good way around my current problem