PreCategory := (forall x y z (m1 : morphism X y z) (m2 : morphism X x y), F x -> G z)%category.
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.