{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              (ι : Type w) →
                (π : ι → α) →
                  (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)) →
                    (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i)) →
                      CategoryTheory.Limits.IsColimit cofan₁ →
                        CategoryTheory.Limits.IsColimit cofan₂ →
                          (m : cofan₁.pt ⟶ cofan₂.pt) →
                            autoParam
                                (∀ (i : ι),
                                  CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
                                    CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i))
                                HomotopicalAlgebra.AttachCells.hm._autoParam →
                              (g₁ : cofan₁.pt ⟶ X₁) →
                                (g₂ : cofan₂.pt ⟶ X₂) →
                                  CategoryTheory.IsPushout g₁ m f g₂ → HomotopicalAlgebra.AttachCells g f