Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adj.counit_naturality_assoc

∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₂.obj} (f : X ⟶ Y) {Z : ↑C₂.obj}
  (h : (CategoryTheory.CategoryStruct.id C₂.obj).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.l.toFunctor.map (α.r.toFunctor.map f))
      (CategoryTheory.CategoryStruct.comp (α.adj.counit.toNatTrans.app Y) h) =
    CategoryTheory.CategoryStruct.comp (α.adj.counit.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp f h)

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Cited by

0 results in Mathlib

Foundations

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