proposition: Proposition fully_faithful_enriched_yoneda : fully_faithful_enriched_functor (enriched_yoneda_enrichment E EqV PV PV').
proof: Proof. intros x y. use make_is_z_isomorphism. - exact (yoneda_inv x y). - split. + exact (yoneda_inv_right x y). + exact (yoneda_inv_left x y). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.EnrichedCats.Examples.Yoneda UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products