Theorems · Theorem · category theory

CategoryTheory.InducedCategory.Hom.ext

∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v, u₂} D} {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} {x y : X.Hom Y}, x.hom = y.hom → x = y

Defined in

Mathlib.CategoryTheory.InducedCategory

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms