Definition yoneda_functor_precomp' : nat_trans (yoneda_objects C c) (functor_composite (functor_opp F) (yoneda_objects D (F c))). Proof. use tpair. - intros d f ; simpl. apply (#F f). - abstract (intros d d' f ; apply funextsec; intro t; simpl; 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.