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$? 



Is the weak inverse of a pseudofunctor between strict 2-categories unique up to pseudonatural equivalence?
**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).


