Functor B A := Build_Functor B A (fun xym__Fx_to_Gy => fun x => xym__Fx_to_Gy x x 1) (fun x__s x__d x__m => fun x => x__m x x 1) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
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.