Theorems · Definition · category theory

CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp

{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} → k.Hom l → l.Hom m → k.Hom m

Composition of morphisms in the Total category.

Defined in

Mathlib.CategoryTheory.Presentable.ColimitPresentation

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category