B\'enabou's theorem for pseudoadjunctions

TL;DR

This paper formalizes Bénabou's theorem within Gray-categories, establishing a precise correspondence between pseudoadjunctions and absolute pseudoextensions, thus advancing the theoretical understanding of higher category structures.

Contribution

It provides a formal account of Bénabou's theorem for pseudoadjunctions in Gray-categories, linking pseudoadjunctions with absolute pseudoextensions.

Findings

Pseudoadjunctions correspond to absolute pseudoextensions in Gray-categories.

The unit of a pseudoadjunction witnesses the pseudoextension.

The paper advances the theoretical framework of higher category theory.

Abstract

We give a formal account of B\'enabou's theorem for peudoadjunctions in the context of Gray-categories. We prove that to give a pseudoadjunction $F \dashv U: A \to X$ with unit $\eta$ in a Gray-category K is precisely to give an absolute left (Kan) pseudoextension $U$ of $1_X$ along $F$ witnessed by $\eta$.