Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adj.right_triangle_components_assoc

∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) (X : ↑C₂.obj) {Z : ↑C₁.obj}
  (h : α.r.toFunctor.obj ((CategoryTheory.CategoryStruct.id C₂.obj).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.adj.unit.toNatTrans.app (α.r.toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp (α.r.toFunctor.map (α.adj.counit.toNatTrans.app X)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (α.r.toFunctor.obj X)) 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