Joint work with Emily Riehl
I've always been very fond of Dubuc's Adjoint Triangle theorems. It seems to me that they are an important, surprisingly useful, and yet oft overlooked tool in the category theory armoury. Indeed, as a canonical example of sheer elegance and beauty in categorical proof making, one can really do no better than Paré's adjoint lifting proof that elementary toposes are finitely cocomplete.
So how might we import these techniques into the world of synthetic ∞-category theory? More specifically, how can we prove such results in the framework provided by ∞-Cosmoi and homotopy coherent monads that Emily Riehl and I have been developing over the past few years? While left adjoint lifting is straightforward by (relatively) elementary means in this context, right adjoint lifting has proved a little more elusive.
Classically, right adjoint lifting entails the construction of a transformation of the monads generated by the adjunctions we are lifting along and, until recently, a natural generalisation of that construction to the ∞-cosmos setting had eluded us. That isn't to say that we didn't have a perfectly workable theory of such transformations to work with, as furnished by Dimitri Zaganidis' elegant diagrammatic description of the -category of homotopy coherent monads. Instead the stumbling block has been entirely one of my own inability to competently drive that beautiful machine.
In this talk we shall discuss a novel way to describe the ∞-double category of lax squares in an ∞-Cosmos and use that to explicate the structure of the -category of homotopy coherent monads and their transformations. In that way we shall largely sidestep Zaganidis' beautiful combinatorics (although it will still arise in applications) and avoid introducing any exotic -structures, beyond those available to us in the (strictly) quasi-category enriched world of ∞-Cosmoi. This allows us to give an entirely elementary account of Dubuc's right adjoint lifting result for ∞-categories living in arbitrary ∞-Cosmoi which I shall conclude this talk with.