∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X₁ X₂ : HomotopicalAlgebra.BifibrantObject C) (f : X₁ ⟶ X₂),
  HomotopicalAlgebra.BifibrantObject.toHoCat.map
      (CategoryTheory.CategoryStruct.comp f
        (HomotopicalAlgebra.BifibrantObject.homMk
          (HomotopicalAlgebra.CofibrantObject.mk X₂.obj).iBifibrantResolutionObj.hom)) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map
      (CategoryTheory.CategoryStruct.comp
        (HomotopicalAlgebra.BifibrantObject.homMk
          (HomotopicalAlgebra.CofibrantObject.mk X₁.obj).iBifibrantResolutionObj.hom)
        (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap
          (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.map f)))