Functor B C. Proof. refine (Build_Functor B C (fun xym__Fx_to_Gy => fun x y z m1 m2 => xym__Fx_to_Gy y z m1 o p_morphism_of F m2)%functor (fun xym__s xym__d xym__m => fun x y z m1 m2 => xym__m y z m1 oR p_morphism_of F m2) _ _); simpl; repeat (intro || apply path_forall); [ apply composition_of_whisker_r | apply whisker_r_left_identity ]. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Pseudofunctor.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import Functor.Composition.Core. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import NaturalTransformation.Identity.