Theorems · Theorem · category theory

CategoryTheory.rightAdjointMate_comp_evaluation

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (fᘁ) X) (ε_ X Xᘁ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ f) (ε_ Y Yᘁ)

Defined in

Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.HasRightDualCategoryTheory.HasRightDual