{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₂} → (c : HomotopicalAlgebra.AttachCells g f) → (i : c.ι) → B (c.π i) ⟶ X₂