Theorems · Theorem · category theory

CategoryTheory.Limits.Fork.IsLimit.hom_ext

∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι → k = l

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category