∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cocone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (e : J ≌ K)
  (w : e.functor.comp G ≅ F),
  (P.coconePointsIsoOfEquivalence Q e w).hom =
    P.desc ((CategoryTheory.Limits.Cocones.equivalenceOfReindexing e w).functor.obj t)