Commit 2024-01-05 14:50 b180173c

feat(Algebra/Homology): morphisms from the homotopy cofiber (#9447) In this PR, we obtain HomologicalComplex.homotopyCofiber.descEquiv which expresses that if φ : F ⟶ G is a morphism of homological complexes, then a morphism homotopyCofiber φ ⟶ K is uniquely determined by a morphism α : G ⟶ K and a homotopy from φ ≫ α to 0.