{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        (F : CategoryTheory.Functor J C) →
                          (isoBot : F.obj ⊥ ≅ X) →
                            autoParam F.IsWellOrderContinuous
                                CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous._autoParam →
                              (incl : F ⟶ (CategoryTheory.Functor.const J).obj Y) →
                                CategoryTheory.Limits.IsColimit { pt := Y, ι := incl } →
                                  autoParam (CategoryTheory.CategoryStruct.comp isoBot.inv (incl.app ⊥) = f)
                                      CategoryTheory.TransfiniteCompositionOfShape.fac._autoParam →
                                    ((j : J) →
                                        ¬IsMax j →
                                          HomotopicalAlgebra.AttachCells (basicCell j)
                                            (F.map (CategoryTheory.homOfLE ⋯))) →
                                      HomotopicalAlgebra.RelativeCellComplex basicCell f