proposition: Lemma is_functor_yoneda (C : category) : is_functor (yoneda_functor_data C).
proof: Proof. unfold is_functor. repeat split; simpl. intro a. set (T:= nat_trans_eq (C:=C^op) (has_homsets_HSET)). simpl. apply T. intro c; apply funextsec; intro f. apply id_right. intros a b c f g. set (T:=nat_trans_eq (C:=C^op) (has_homsets_HSET)). apply T. simpl; intro d; apply funextsec; intro h. apply assoc. 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