category_theory.adjunction

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.