{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₂} →
              {motive : HomotopicalAlgebra.AttachCells g f → Sort u_1} →
                (t : HomotopicalAlgebra.AttachCells g f) →
                  ((ι : Type w) →
                      (π : ι → α) →
                        (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)) →
                          (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i)) →
                            (isColimit₁ : CategoryTheory.Limits.IsColimit cofan₁) →
                              (isColimit₂ : CategoryTheory.Limits.IsColimit cofan₂) →
                                (m : cofan₁.pt ⟶ cofan₂.pt) →
                                  (hm :
                                      ∀ (i : ι),
                                        CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
                                          CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i)) →
                                    (g₁ : cofan₁.pt ⟶ X₁) →
                                      (g₂ : cofan₂.pt ⟶ X₂) →
                                        (isPushout : CategoryTheory.IsPushout g₁ m f g₂) →
                                          motive
                                            { ι := ι, π := π, cofan₁ := cofan₁, cofan₂ := cofan₂,
                                              isColimit₁ := isColimit₁, isColimit₂ := isColimit₂, m := m, hm := hm,
                                              g₁ := g₁, g₂ := g₂, isPushout := isPushout }) →
                    motive t