proposition: Lemma yoneda_map_1_2 (C : category) (c : C) (F : functor C^op HSET) (alpha : hom _ (yoneda C c) F) : yoneda_map_2 _ _ _ (yoneda_map_1 _ _ _ alpha) = alpha.
proof: Proof. simpl in *. set (T:=nat_trans_eq (C:=C^op) (has_homsets_HSET)). apply T. intro a'; simpl. apply funextsec; intro f. unfold yoneda_map_1. intermediate_path ((alpha c · #F f) (identity c)). apply idpath. rewrite <- nat_trans_ax. unf; apply maponpaths. apply (id_right f ). 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