Definition yoneda_ob_functor_data (C : category) (c : C) : functor_data (C^op) HSET. Proof. exists (λ c', make_hSet (yoneda_objects_ob C c c') (homset_property C _ _ ) ). intros a b f g. unfold yoneda_objects_ob in *. simpl in *. exact (f · g). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.whiskering.