Theorems · Theorem · category theory

CategoryTheory.Arrow.RightHomotopy.ext

∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {x y : CategoryTheory.Arrow.RightHomotopy f g}, x.hom = y.hom → x = y

Defined in

Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses no axioms