{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₂} → (self : HomotopicalAlgebra.AttachCells g f) → CategoryTheory.Limits.IsColimit self.cofan₂