Re: biadjoint biequivalences and spans in 2-categories

[Richard Garner <rhgg2@hermes.cam.ac.uk>]

> At the beginning of section 3 he defines a bicategory of spans from A to
> B in any bicategory, and given finite bilimits, essentially describes
> how to construct what one might call an "unbiased tricategory" of spans
> (of course, the definition of tricategory didn't exist at the time).
>
> He doesn't give any details of the proofs, but one could probably
> construct a detailed proof from these ideas without much more than
> tedium.  I don't know whether anyone has written them out.

One amusing thing about the tricategory of spans in a
2-category, with composition by iso-comma object, is that it
is barely a tricategory. Binary composition is associative up
to iso; it is only the unitality which is really up to
equivalence. Something similar happens if you define a
tricategory of biprofunctors.

Richard