object ((C -> C') -> (C' -> D) -> (C -> D)) := Functor.
Require Import Category.Core Functor.Core. Require Import FunctorCategory.Core. Require Import Functor.Composition.Functorial.Core. Require Import UniversalProperties.