`{Funext} A (F : object (A -> set_cat)) a : morphism set_cat (F a) (coyoneda_functor A F a). Proof. intro Fa. hnf. simpl in *. let F0 := match goal with |- NaturalTransformation ?F ?G => constr:(F) end in let G0 := match goal with |- NaturalTransformation ?F ?G => constr:(G) end in refine (Build_NaturalTransformation F0 G0 (fun a' : A => (fun f : morphism A a a' => F _1 f Fa)) _ ). simpl. abstract ( repeat first [ reflexivity | intro | apply path_forall | progress rewrite ?composition_of, ?identity_of ] ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Dual Functor.Dual. Require Import Functor.Composition.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import SetCategory. Require Import Functor.Attributes. Require Import Functor.Composition.Functorial. Require Import Functor.Identity. Require Import HomFunctor. Require Import FunctorCategory.Core. Require Import NaturalTransformation.Paths. Require Import HoTT.Tactics.