Require Import Category.Core Functor.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import Functor.Composition.Core Functor.Identity. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import FunctorCategory.Core.