Definition functor_composite_functor {A B C:category} (F:A⟶B) : [B,C] ⟶ [A,C]. Proof. unshelve refine (makeFunctor _ _ _ _). - exact (λ G, F ∙ G). - intros G G' p; simpl. unshelve refine (@makeNattrans A C (F ∙ G) (F ∙ G') (λ a, p ◽ (F ◾ a)) _). abstract ( intros a a' f; rewrite 2? nattrans_nattrans_object_assoc; exact (nattrans_naturality p (F ▭ f))) using _L_. - abstract ( intros G; now apply (nat_trans_eq (homset_property C))) using _M_. - abstract ( intros G G' G'' p q; now apply (nat_trans_eq (homset_property C))) using _N_. Defined.
Require Import UniMath.MoreFoundations.Tactics.