Theorems · Theorem · category theory

CategoryTheory.CostructuredArrow.IsUniversal.hom_ext

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) {c : C}
  {η η' : c ⟶ f.left},
  CategoryTheory.CategoryStruct.comp (S.map η) f.hom = CategoryTheory.CategoryStruct.comp (S.map η') f.hom → η = η'

Two morphisms into a universal S-costructured arrow are equal if their image under S are equal after postcomposing the universal arrow.

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category