{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            c.toCostructuredArrow.comp
                ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (CategoryTheory.Over.forget c.pt)) ≅
              F