Theorems · Theorem · category theory

CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_hom_apply_app

∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  (X : (CategoryTheory.Functor J C)ᵒᵖ) (X_1 : C)
  (a : CategoryTheory.Limits.limit ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X_1))) (j : J),
  ((CategoryTheory.ConcreteCategory.hom
            (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X_1))
          a).app
      j =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X_1)) (Opposite.op j)))
      a

Defined in

Mathlib.CategoryTheory.Limits.Types.Yoneda

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Category