Theorems · Theorem · category theory

Homotopy.ext

∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V}
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {x y : Homotopy f g}, x.hom = y.hom → x = y

Defined in

Mathlib.Algebra.Homology.Homotopy

Cited by

4 results in Mathlib

Foundations

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