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 toOverCompYoneda (A : Cᵒᵖ ⥤ Type v) (T : Over A) :
(CostructuredArrow.toOver yoneda A).op ⋙ yoneda.obj T ≅
yoneda.op ⋙ yoneda.obj ((overEquivPresheafCostructuredArrow A).functor.obj T) :=
NatIso.ofComponents
(fun X =>
(overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
(Iso.homCongr ((CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).app X.unop)
(Iso.refl _)).toIso)
(by cat_disch)
