Ordinary adjoint functors as bicategorical adjunctions

Categories, functors, and natural transformations form the bicategory Cat. Mathlib supplies Adjunction.toCat and Adjunction.ofCat; this file packages those mutually inverse conversions as an equivalence. Thus ordinary adjoint functors are a specialization of the canonical bicategorical notion, not a second repository-owned hierarchy.

def CategoryTheory.Adjunction.bicategoricalEquiv {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F : Functor C D} {G : Functor D C} : (F ⊣ G) ≃ Bicategory.Adjunction F.toCatHom G.toCatHom

Ordinary adjunctions between F and G are exactly adjunctions between the corresponding 1-morphisms in the bicategory Cat.

Equations

• CategoryTheory.Adjunction.bicategoricalEquiv = { toFun := CategoryTheory.Adjunction.toCat, invFun := CategoryTheory.Adjunction.ofCat, left_inv := ⋯, right_inv := ⋯ }