English
There is an isomorphism between the presheaf of enriched natural transformations between F and G and the Yoneda object of the enriched hom between the corresponding enriched functors.
Русский
Существует изоморфизм между прешафом обогащённых натрансформаций между F и G и Янода-объектом соответствующей обогащённой гом‑множества между этими функторaми.
LaTeX
$$$\\mathrm{enrichedNatTransYoneda}(F,G) \\cong \\mathrm{yoneda}\\bigl(\\mathrm{enrichedFunctorTypeEquivFunctor}(F) \\to \\mathrm{enrichedFunctorTypeEquivFunctor}(G)\\bigr)$$$
Lean4
/-- We verify that the presheaf representing natural transformations
between `Type v`-enriched functors is actually represented by
the usual type of natural transformations!
-/
def enrichedNatTransYonedaTypeIsoYonedaNatTrans {C : Type v} [EnrichedCategory (Type v) C] {D : Type v}
[EnrichedCategory (Type v) D] (F G : EnrichedFunctor (Type v) C D) :
enrichedNatTransYoneda F G ≅ yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G) :=
NatIso.ofComponents
(fun α =>
{ hom := fun σ x =>
{ app := fun X => σ.app X x
naturality := fun X Y f => congr_fun (σ.naturality X Y) ⟨x, f⟩ }
inv := fun σ =>
{ app := fun X x => (σ x).app X
naturality := fun X Y => by ext ⟨x, f⟩; exact (σ x).naturality f } })
(by cat_disch)
