There are many ways to give a definition of a biadjunction. For instance, one may say that a pseudofunctor $F:\mathcal{C}\rightarrow \mathcal{D}$ is left biadjoint to $G:\mathcal{D}\rightarrow \mathcal{C}$ if there are pseudo-natural transformations $\eta:Id_{\mathcal{C}}\rightarrow GF$ and $\epsilon:FG\rightarrow Id_{\mathcal{D}}$ satisfying the triangle identities up to invertible modifications.
Now, there is also a coherent version of the latter definition (see Gurski), where the modifications witnessing the triangle identites satisfy the swallowtail equations. The ncatlab entry for biadjunctions (and my intuition) makes me believe that every biadjunction can be made coherent, but I haven't been able to find a reference in the litterature. Does anybody know where to find one?
