Theorems · Theorem · category theory

CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y),
  (CategoryTheory.tensorRightHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (ᘁY) Y ᘁX).symm
      (CategoryTheory.CategoryStruct.comp (η_ (ᘁX) X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁX) f)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ᘁY).hom (ᘁf)

Defined in

Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.HasLeftDualCategoryTheory.HasLeftDual