Re: cleavages and choice

[Toby Bartels <categories@TobyBartels.name>]

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