proposition: Lemma is_natural_yoneda_iso_inv (C : category) (F : functor C^op HSET): is_nat_trans F (yoneda_iso_target C F) (λ c, yoneda_map_2 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_map_2. intro A. apply nat_trans_eq. { apply (has_homsets_HSET). } cbn. intro d. apply funextfun. unfold yoneda_objects_ob. intro g. unfold yoneda_morphisms_data. apply (! toforallpaths _ _ _ (functor_comp F _ _ ) A). 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