{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            {D : Type u₄} →
              [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
                (G : CategoryTheory.Functor C D) →
                  [G.Faithful] →
                    (ht : CategoryTheory.Limits.IsColimit (G.mapCocone t)) →
                      (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) →
                        (∀ (s : CategoryTheory.Limits.Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)) →
                          CategoryTheory.Limits.IsColimit t