Theorems · Definition · category theory

CategoryTheory.Adjunction.toCat

{C D : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      {F : CategoryTheory.Functor C D} →
        {G : CategoryTheory.Functor D C} → (F ⊣ G) → CategoryTheory.Bicategory.Adjunction F.toCatHom G.toCatHom

The adjunction in the bicategorical sense attached to an adjunction between functors.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Cited by

14 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category