Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adjunction.ofCat_comp

∀ {C D E : CategoryTheory.Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : CategoryTheory.Bicategory.Adjunction F G) {F' : D ⟶ E}
  {G' : E ⟶ D} (adj' : CategoryTheory.Bicategory.Adjunction F' G'),
  CategoryTheory.Adjunction.ofCat (adj.comp adj') =
    (CategoryTheory.Adjunction.ofCat adj).comp (CategoryTheory.Adjunction.ofCat adj')

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Cited by

0 results in Mathlib

Foundations

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