{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      {c : F.CoconeTypes} →
        {motive : c.IsColimitCore → Sort u_1} →
          ((desc : (c' : F.CoconeTypes) → c.pt → c'.pt) →
              (fac : ∀ (c' : F.CoconeTypes) (j : J), desc c' ∘ c.ι j = c'.ι j) →
                (funext : ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g) →
                  motive { desc := desc, fac := fac, funext := funext }) →
            (t : c.IsColimitCore) → motive t