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} {f g : X ⟶ Y}, f.hom = g.hom → f = g

Defined in

Mathlib.CategoryTheory.InducedCategory

Cited by

16 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.Category