Theorems · Theorem · category theory

CategoryTheory.StructuredArrow.IsUniversal.hom_ext

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

Two morphisms out of a universal T-structured arrow are equal if their image under T are equal after precomposing the universal arrow.

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category