mathlib3

87ab09ca - feat(category_theory/abelian/injective_resolution): homotopy between descents of morphism and two injective resolutions (#12743)

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.