proposition: Lemma is_z_iso_yoneda_functor_precomp : is_z_isomorphism yoneda_functor_precomp.
proof: Proof. apply nat_trafo_z_iso_if_pointwise_z_iso. intro a. simpl. set (T:= make_weq _ (Fff a c)). set (TA := make_hSet (hom C a c) (homset_property C _ _)). set (TB := make_hSet (hom D (F a) (F c)) (homset_property _ _ _ )). apply (hset_equiv_is_z_iso TA TB T). Defined.
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