Definition yoneda_functor_precomp_nat_trans : @nat_trans C [C^op, HSET, (has_homsets_HSET)] (yoneda C) (functor_composite A B). Proof. use tpair. - intro c; simpl. apply yoneda_functor_precomp. - abstract ( intros c c' f; apply nat_trans_eq; [apply (has_homsets_HSET) |]; intro d; apply funextsec; intro t; cbn; apply functor_comp). 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.