Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I am looking for a proof of the fact that a bifunctor between bicategories is an biequivalence if and only if it is fully faithful and essentially surjective (in the appropriate sense) that I can cite. Does anyone know a source?
By bifunctor you mean pseudofunctor or 2-functor?
I think Gurski has something on it. Street defines a biequivalence to be ff+eso in ’Fibrations in bicategories’, and Gurski says in “An algebraic theory of tricategories”
It should now be clear that our definition of biadjoint biequivalence, in the case of the tricategory Bicat, is a fully algebraic version of the combination of biequivalence and biadjunction as given by Street in [37].
([37] is Street’s fibrations article). I don’t know of a formal proof, though.
I would call it folklore. It’s easy to prove, by analogy with (and making use of) the corresponding fact for categories.
BTW, I don’t think anyone uses “bifunctor” for a functor between bicategories. The classical term was “homomorphism” (for a map that is functorial up to coherent iso) but nowadays I think the preferred thing to say is just “functor,” that being the most sensible notion of functor between bicategories.
Mike: Haha, I usually use ’Functor’ and ’equivalence’ but I thought for that post I am on the safe side if I add the prefix bi- everywhere ;)
Its clear that it is relatively simple to proof that fact (given the right axiom of choice) but I wonder that no one has written it up.
Nobody uses “bifunctor” in this meaning just because the latter term is used in another meaning (a functor from the product category).
Zoran’s comment should be a genearlisation of the classical term ‘bifunction’, although right now I can’t find any evidence for that term. (I can find ‘binary function’, however.)
But yes, Thomas’s bifunctors are Harry’s pseudofunctors.
given the right axiom of choice
Or given a suitable anafunctor-like definition (ana-2-functors).
1 to 7 of 7