Dear Toby, The theory of monoidal categories and bicategories is already written. I may be interested in working with them, even though it is unpleasant to recur to choice for most (non-strict) structures of these kinds. I have no interest in rewriting these theories in a different shape, using anafunctors or similar tools, or even study such variations if someone has given them. Of course other people may prefer the way you are saying. I just wanted to point out that there are many occasions where we are led to use choice - at least if we want to stay within 'classical' category theory, as expounded - say - in Mac Lane's text. Regards, Marco On 03/ago/2014, at 18.30, Toby Bartels wrote:
Marco Grandis <grandis@dima.unige.it> wrote in part:
Yet you cannot define a bicategory of spans without assuming that such a choice has been made; in the same way as you cannot define the (good) monoidal structure of Ab without recurring to a choice of tensor products.
A monoidal structure on a category C is a functor C x C -> C, an object of C (aka a functor 1 -> C), and various natural transformations satisfying some equations. If by "functor" we mean an anafunctor, then no choice is needed.
Presumably you are thinking along these lines when you write
Unless you want to redefine bicategories replacing the composition of arrows with an existence property.
My point is that anafunctors tell you automatically what to do.
Better yet, working in HoTT tells you automatically what to do. All of this only looks complicated from a set-based perspective.
--Toby
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]