Theorems · Theorem · category theory

CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_base

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} (f : k.Hom l) (g : l.Hom m),
  (f.comp g).base = CategoryTheory.CategoryStruct.comp f.base g.base

Defined in

Mathlib.CategoryTheory.Presentable.ColimitPresentation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category