Bénabou's theorem for pseudoadjunctions

Matěj Dostál

We give a formal account of Bénabou's theorem for peudoadjunctions in the context of Gray-categories. We prove that to give a pseudoadjunction $F⊣U:A\to X$ with unit $\eta$ i…