NaturalTransformation (hom_functor C) (hom_functor D o (F^op, F)). Proof. refine (Build_NaturalTransformation (hom_functor C) (hom_functor D o (F^op, F)) (fun (sd : object (C^op * C)) m => (F _1 m)%morphism) _ ). abstract ( repeat (intros [] || intro); simpl in *; repeat (apply path_forall; intro); simpl; rewrite !composition_of; reflexivity ). Defined.
Require Import Category.Core Functor.Core HomFunctor Category.Morphisms Category.Dual Functor.Dual Category.Prod Functor.Prod NaturalTransformation.Core SetCategory.Core Functor.Composition.Core. Require Import Basics.Trunc Types.Universe HIT.iso HoTT.Truncations.Core.