∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (x x_1 : HomotopicalAlgebra.CofibrantObject C) (f : x ⟶ x_1),
  HomotopicalAlgebra.CofibrantObject.toHoCat.map
      (CategoryTheory.CategoryStruct.comp
        (HomotopicalAlgebra.CofibrantObject.homMk
          (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap (HomotopicalAlgebra.CofibrantObject.ι.map f)))
        {
          hom :=
            HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj (HomotopicalAlgebra.CofibrantObject.ι.obj x_1) }) =
    HomotopicalAlgebra.CofibrantObject.toHoCat.map
      (CategoryTheory.CategoryStruct.comp
        { hom := HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj (HomotopicalAlgebra.CofibrantObject.ι.obj x) }
        f)