Lean4
/-- This isomorphism says that hom-sets in the category `Over A` for a presheaf `A` where the domain
is of the form `(CostructuredArrow.toOver yoneda A).obj X` can instead be interpreted as
hom-sets in the category `(CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` where the domain is of the
form `yoneda.obj X` after adjusting the codomain accordingly. This is desirable because in the
latter case the Yoneda lemma can be applied. -/
def toOverCompCoyoneda (A : Cᵒᵖ ⥤ Type v) :
(CostructuredArrow.toOver yoneda A).op ⋙ coyoneda ≅
yoneda.op ⋙ coyoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (overEquivPresheafCostructuredArrow A).functor :=
NatIso.ofComponents
(fun X =>
NatIso.ofComponents
(fun Y =>
(overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
(Iso.homCongr ((CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).app X.unop)
(Iso.refl _)).toIso))
(by cat_disch)
