Bicategories, pseudofunctors, and biequivalences

A bicategory $\mathcal{B}$ consists of: a class of objects; for every ordered pair $X,Y$ a category $\mathcal{B}(X,Y)$ whose objects are 1-cells $X\to Y$ and whose morphisms are 2-cells; identity 1-cells $1_X:X\to X$; composition functors $c_{X,Y,Z}:\mathcal{B}(Y,Z)\times \mathcal{B}(X,Y)\to \mathcal{B}(X,Z)$, written $g\circ f$ on 1-cells and $\beta \ast \alpha$ on 2-cells; and invertible natural transformations (the associator and the two unitors) ${\alpha }_{h,g,f}:(h\circ g)\circ f\Rightarrow h\circ (g\circ f),{\lambda }_f:1_Y\circ f\Rightarrow f,{\rho }_f:f\circ 1_X\Rightarrow f,$ satisfying the pentagon identity ${\alpha }_{k,h,g\circ f}{\alpha }_{k\circ h,g,f}=(1_k\ast {\alpha }_{h,g,f}){\alpha }_{k,h\circ g,f}({\alpha }_{k,h,g}\ast 1_f)$ and the triangle identity $(1_g\ast {\lambda }_f){\alpha }_{g,1_B,f}={\rho }_g\ast 1_f$, with composition of 2-cells read right to left. A pseudofunctor $F:\mathcal{B}\to {\mathcal{B}}^{\mathrm{\prime }}$ consists of a function on objects, functors $\mathcal{B}(X,Y)\to {\mathcal{B}}^{\mathrm{\prime }}(FX,FY)$, and invertible comparison 2-cells ${\varphi }_{g,f}:F(g)\circ F(f)\Rightarrow F(g\circ f)$ and ${\varphi }_X:1_{FX}^{\mathrm{\prime }}\Rightarrow F(1_X)$ natural in the composable 1-cells: for $u:f\Rightarrow f\mathrm{\prime }$ and $v:g\Rightarrow g\mathrm{\prime }$ one requires $F(v\ast u){\varphi }_{g,f}={\varphi }_{g\mathrm{\prime },f\mathrm{\prime }}(F(v)\ast F(u))$. They satisfy $F({\alpha }_{h,g,f}){\varphi }_{h\circ g,f}({\varphi }_{h,g}\ast 1_{F(f)})={\varphi }_{h,g\circ f}(1_{F(h)}\ast {\varphi }_{g,f}){\alpha }_{F(h),F(g),F(f)}^{\mathrm{\prime }},$ $F({\lambda }_f){\varphi }_{1_B,f}({\varphi }_B\ast 1_{F(f)})={\lambda }_{F(f)}^{\mathrm{\prime }},F({\rho }_f){\varphi }_{f,1_A}(1_{F(f)}\ast {\varphi }_A)={\rho }_{F(f)}^{\mathrm{\prime }}\mathrm{.}$ Two objects $X,Y$ of a bicategory are equivalent when there are 1-cells $f:X\to Y$ and $g:Y\to X$ together with invertible 2-cells $1_X\Rightarrow g\circ f$ and $f\circ g\Rightarrow 1_Y$. A pseudofunctor $F:\mathcal{B}\to {\mathcal{B}}^{\mathrm{\prime }}$ is a biequivalence when every local functor $\mathcal{B}(X,Y)\to {\mathcal{B}}^{\mathrm{\prime }}(FX,FY)$ is an equivalence of categories and every object of ${\mathcal{B}}^{\mathrm{\prime }}$ is equivalent to $FY$ for some object $Y$ of $\mathcal{B}$. A strict 2-category is the special case of a bicategory in which all associators and unitors are identities (Strict 2-category); a one-object bicategory is exactly a monoidal category (Monoidal category). The definition asserts these axioms on supplied data; it does not assert that any particular tensor construction satisfies them, and it uses no choice.