PreCategory := @Build_PreCategory (Functor C D) (@NaturalTransformation C D) (@identity C D) (@compose C D) (@associativity _ C D) (@left_identity _ C D) (@right_identity _ C D) _.
Require Import Category.Strict Functor.Core NaturalTransformation.Core Functor.Paths. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Identity NaturalTransformation.Composition.Laws NaturalTransformation.Paths.