Theorems · Theorem · category theory

CategoryTheory.Enriched.Functor.associator_inv_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L M N : CategoryTheory.Functor C D) {X : C}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N))).obj
      X),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((K.homObjFunctor L).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
            ((L.homObjFunctor M).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
            ((M.homObjFunctor N).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))).inv)
      x =
    ((x.1, x.2.1), x.2.2)

Defined in

Mathlib.CategoryTheory.Functor.FunctorHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category