proposition: Lemma is_natural_yoneda_iso (C : category) (F : functor C^op HSET): is_nat_trans (yoneda_iso_target C F) F (λ c, yoneda_map_1 C c F).
proof: Proof. unfold is_nat_trans. intros c c' f. cbn in *. apply funextsec. unfold yoneda_ob_functor_data. cbn. unfold yoneda_morphisms_data. unfold yoneda_map_1. intro X. assert (XH := nat_trans_ax X). cbn in XH. unfold yoneda_objects_ob in XH. assert (XH' := XH c' c' (identity _ )). assert (XH2 := toforallpaths _ _ _ XH'). rewrite XH2. rewrite (functor_id F). cbn. clear XH2 XH'. assert (XH' := XH _ _ f). assert (XH2 := toforallpaths _ _ _ XH'). eapply pathscomp0. 2: apply XH2. rewrite id_right. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.whiskering