∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.limitRightOpIsoOpColimit F =
    CategoryTheory.Limits.limit.isoLimitCone
      { cone := CategoryTheory.Limits.coneRightOpOfCocone (CategoryTheory.Limits.colimit.cocone F),
        isLimit := CategoryTheory.Limits.isLimitConeRightOpOfCocone F (CategoryTheory.Limits.colimit.isColimit F) }