Re: cleavages and choice

[Marco Grandis <grandis@dima.unige.it>]

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/ ]