Lean4
/-- Naturally in `X`, we have `Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi)`, where `Y` is the
"Yoneda embedding" `CostructuredArrow.toOver yoneda A`. This is a relative version of
`yonedaYonedaColimit`. -/
noncomputable def toOverCompYonedaColimit :
(CostructuredArrow.toOver yoneda A).op ⋙ yoneda.obj (colimit F) ≅
(CostructuredArrow.toOver yoneda A).op ⋙ colimit (F ⋙ yoneda) :=
calc
(CostructuredArrow.toOver yoneda A).op ⋙ yoneda.obj (colimit F) ≅ yoneda.op ⋙ yoneda.obj (E.obj (colimit F)) :=
CostructuredArrow.toOverCompYoneda A _
_ ≅ yoneda.op ⋙ yoneda.obj (colimit (F ⋙ E)) :=
(Functor.isoWhiskerLeft yoneda.op (yoneda.mapIso (preservesColimitIso E F)))
_ ≅ yoneda.op ⋙ colimit ((F ⋙ E) ⋙ yoneda) := (yonedaYonedaColimit _)
_ ≅ yoneda.op ⋙ ((F ⋙ E) ⋙ yoneda).flip ⋙ colim := (Functor.isoWhiskerLeft _ (colimitIsoFlipCompColim _))
_ ≅ (yoneda.op ⋙ coyoneda ⋙ (Functor.whiskeringLeft _ _ _).obj E) ⋙ (Functor.whiskeringLeft _ _ _).obj F ⋙ colim :=
(Iso.refl _)
_ ≅ (CostructuredArrow.toOver yoneda A).op ⋙ coyoneda ⋙ (Functor.whiskeringLeft _ _ _).obj F ⋙ colim :=
(Functor.isoWhiskerRight (CostructuredArrow.toOverCompCoyoneda _).symm _)
_ ≅ (CostructuredArrow.toOver yoneda A).op ⋙ (F ⋙ yoneda).flip ⋙ colim := (Iso.refl _)
_ ≅ (CostructuredArrow.toOver yoneda A).op ⋙ colimit (F ⋙ yoneda) :=
Functor.isoWhiskerLeft _ (colimitIsoFlipCompColim _).symm
