Require Import Category.Core Functor.Core. Require Import Adjoint.UnitCounit. Require Import Functor.Dual. Require Import Functor.Prod.Core. Require Import HomFunctor. Require Import Functor.Composition.Core. Require Import FunctorCategory.Morphisms. Require Import Functor.Identity.