Theorems · Theorem · category theory

CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Y Z : C}
  [inst_2 : CategoryTheory.HasLeftDual Z] (f : Y ⟶ ᘁZ),
  (CategoryTheory.tensorLeftHomEquiv Y (ᘁZ) Z (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) (ε_ (ᘁZ) Z)) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.rightUnitor ᘁZ).inv

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.HasLeftDual