Theorems · Theorem · category theory

CategoryTheory.Limits.end_.map_comp_assoc

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasEnd F'] (f : F ⟶ F')
  {F'' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_4 : CategoryTheory.Limits.HasEnd F'']
  (g : F' ⟶ F'') {Z : C} (h : CategoryTheory.Limits.end_ F'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map (CategoryTheory.CategoryStruct.comp f g)) h

Defined in

Mathlib.CategoryTheory.Limits.Shapes.End

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasEndCategoryTheory.Limits.HasEndCategoryTheory.Limits.HasEnd