Theorems · Theorem · category theory

CategoryTheory.Limits.Cofan.IsColimit.hom_ext

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

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

16 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category