Is the weak inverse of a pseudofunctor between strict 2-categories unique up to pseudonatural equivalence? Suppose $F: C \rightarrow D$ is a pseudofunctor which induces an equivalence of 2-categories then there exists a pseduofunctor $G: D \rightarrow C$ and pseudonatural equivalences $FG \Rightarrow id_D$ and $GF \Rightarrow id_C$.
If $H: D \Rightarrow C$ is another pseudofunctor and there exists pseudonatural equivalences $FH \Rightarrow id_D$ and $HF \Rightarrow id_C$ is it true that there exists a pseudonatural equivalence $H \Rightarrow G$? 
 A: Yes, and they can be arbitrary bicategories, not strict 2-categories.
There’s a tricategory Bicat of bicategories, pseudofunctors, pseudo-natural transformations, and modifications; so working in this tricategory, we can run the usual argument for uniqueness (up to an invertible higher cell) of a two-sided inverse:
$$ H \simeq H \cdot 1_D \simeq H \cdot (F \cdot G) \simeq (H \cdot F) \cdot G \simeq 1_C \cdot G \simeq G.$$
If you don’t want to rely on the full theorem that bicategories form a tricategory, then you can of course just check the few specific aspects of it that are required here (i.e. whiskering, the unitors, and the associator).
Edit.  I realise I missed mentioning one subtlety: we’re also relying on the fact that any pseudo-natural equivalence has a pseudo-natural quasi-inverse.  So if we were using strictly natural transformations, or if we didn’t want to use AC, we’d be stuck at this step.  I don’t know the answer to your question if one makes either of those changes to the setup (though for the working-without-choice setting, my preferred answer would be: we should have set it all up using ana-functors).
