On biadjoint triangles with additional modifications
Gabriel Merlin
TL;DR
This work extends Dubuc’s adjoint triangle theorem to a bicategorical setting by leveraging descent objects and an additional modification cell, and shows that the desired left biadjoint to a pseudofunctor $\mathbf{G}$ can be obtained as the inverter of this extra datum under suitable hypotheses. The main result demonstrates how to construct the unit and counit of the lifted biadjunction through inverter properties and a careful arrangement of pseudonatural transformations and invertible modifications, with two triangle laws encoded as coherence data. A key simplification occurs when the left biadjoint functor $\mathbf{G}$ is fully faithful, allowing a more direct, objectwise approach and reducing reliance on descent-type hypotheses. The paper also applies the theory to Kleisli bicategories arising from KZ-monads, showing that the inclusion pseudofunctor of inverter objects has a left biadjoint under preservation of pseudomonicity, and supports all results with a Coq formalization. These contributions advance understanding of adjoint-like phenomena in higher-category contexts and provide concrete tools for constructing biadjoints in bicategorical settings with descent-like data.
Abstract
Lucatelli Nunes obtained a 2-categorical version of the adjoint triangle theorem of Dubuc using the descent object of a specific diagram. In some cases, such a diagram can be filled with an extra cell. We show then how to obtain a biadjoint as an inverter of this additional datum (under suitable hypotheses). The problem addressed here is slightly different however: we still have a triangle of pseudofunctors but the lifted biadjoint is not the same. The construction is simplified when the pseudofunctor whose left biadjoint is sought is fully faithful. As an example, we get the biadjoint of the inclusion pseudofunctor of a bicategory associated to a KZ-monad preserving pseudomonicity.