envelope of an adjunction

Let be a pair of adjoint functors (an adjunction in Cat). The envelope of the adjunction, denoted , is the category whose objects are quadruples such that and are each other’s mate, and whose morphisms are pairs such that or equivalently . A functor is left adjoint to a functor if and only if there is an isomorphism of comma categories and this isomorphism commutes with the forgetful functors to the product category (see there). In this case, the envelope is also isomorphic to these comma...