Commit 2022-03-17 07:17 87ab09ca
View on Github →feat(category_theory/abelian/injective_resolution): homotopy between descents of morphism and two injective resolutions (#12743) This pr contains the following
category_theory.InjectiveResolution.desc_homotopy: Any two descents of the same morphism are homotopic.category_theory.InjectiveResolution.homotopy_equiv: Any two injective resolutions of the same object are homotopically equivalent.