Functor A B. Proof. refine (Build_Functor A B (fun x__Fx_to_Gx => fun x y m => p_morphism_of G m o x__Fx_to_Gx x)%functor (fun x__s x__d x__m => fun x y m => p_morphism_of G m oL x__m x) _ _); simpl; repeat (intro || apply path_forall); [ apply composition_of_whisker_l | apply whisker_l_right_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.