Dealing with two competing conventions

[patrick-nicodemus]

While working on the development of bicategories I noticed the following infelicity.

In 1-cats, whiskering is a primitive notion and horizontal composition of 2-cells is a derived notion. Specifically, for C a 1-cat, given a, b, c : C and f g : a $-> b, h k : b $-> c, p : f $== g and q : h $== k, we define cat_comp2 p q as (q $@R f) $@ (k $@L p) .

On the other hand, there is is0functor_prod_is0functor defined in WildCat/Prod.v, which can be used for any F : A -> B -> C, whenever A, B are both graphs and C is a 01-cat; if F is a graph homomorphism in each argument separately while the other is held constant, then one can define a graph homomorphism (uncurry F) : A * B -> C by (f,g) |-> (F f b') $o (F a g). This is in turn used widely in the library, indirectly through Build_Is0Bifunctor''.

The infelicity here is that these conventions don't agree, i.e., is0functor_prod_is0functor cat_comp sends (q, p) to (p $@R h) $@ (g $@L q) rather than (q $@R f) $@ (k $@L p) , and life would be better if these two were definitionally equal.

There are several different ways to work around this or fix it.

• Redefine cat_comp2
• Redefine is0functor_prod_is0functor
• Define a second copy of is0functor_prod_is0functor which has the same type but a different implementation, and use this when compatibility with cat_comp is desired / appropriate (and a third constructor Build_Is0Bifunctor''' as well)
• In all cases where compatibility of the bifunctor structure with cat_comp is required, first apply Build_Is0Bifunctor'' to flip (cat_comp), and then define the desired bifunctor structor on cat_comp = flip (flip cat_comp) in terms of the bifunctor structure on flip cat_comp.

I would like some input on what would be the best way to resolve this. I don't have to use Bifunctor.v in the definition of a bicategory, it just seems like a slightly more elegant way of bundling the data.

[jdchristensen]

I think either of the first two options is fine. I suspect that is0functor_prod_is0functor is used less often, so I would try the second option, i.e. changing its definition. But if option one is less work, that would also be fine with me.