Cocontinuity of hom and procoyoneda lemma

Stream: Is there code for X?

[Christian Merten]

Do we have any of the following?

import Mathlib

open CategoryTheory Limits Opposite

universe u₁ u₂ v₁ v₂

variable {C : Type u₁} [Category.{u₂} C] {I : Type v₁} [Category.{v₂} I] (F : I ⥤ C)
variable [HasColimit F] [HasLimit (F.op ⋙ coyoneda)]

instance : HasLimit F.op := hasLimit_op_of_hasColimit F

noncomputable def limitOfOpIsoOpColimit : limit F.op ≅ op <| colimit F :=
  let c : Cocone F := colimit.cocone F
  let hc : IsColimit c := colimit.isColimit F
  limit.isoLimitCone ⟨c.op, IsColimit.op hc⟩

noncomputable def homCocont : coyoneda.obj (limit F.op) ≅ limit (F.op ⋙ coyoneda) :=
  preservesLimitIso coyoneda F.op

noncomputable def homCocont' : coyoneda.obj (op <| colimit F) ≅ limit (F.op ⋙ coyoneda) :=
  coyoneda.mapIso (limitOfOpIsoOpColimit F).symm ≪≫ homCocont F

noncomputable def homCocont'App [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) :
    (colimit F ⟶ A) ≅ limit (F.op ⋙ yoneda.obj A) :=
  ((homCocont' F).app A).trans <| limitObjIsoLimitCompEvaluation _ _

I need it for:

variable {C : Type u₁} [Category.{u₂} C] {J : Type v₁} [Category.{v₂} J] (D : Jᵒᵖ ⥤ C)
variable (F : C ⥤ Type u₂)

variable [HasColimit (D.rightOp ⋙ coyoneda)] [HasLimitsOfShape Jᵒᵖ (Type (max u₁ u₂))]

noncomputable def procoyonedaIso :
    (colimit (D.rightOp ⋙ coyoneda) ⟶ F) ≅ limit (D ⋙ F ⋙ uliftFunctor.{u₁}) :=
  (homCocont'App _ F).trans
    (HasLimit.isoOfNatIso (isoWhiskerLeft (D ⋙ Prod.sectl C F) (coyonedaLemma C)))

If it does not exist, do you have a suggestion where it should go?