Theorems · Theorem · category theory

CategoryTheory.Limits.Cofan.IsColimit.fac

∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F}
  (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

17 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category