fact: Definition functor_category : 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) _.
imports: Category.Strict Functor.Core NaturalTransformation.Core Functor.Paths NaturalTransformation.Composition.Core NaturalTransformation.Identity NaturalTransformation.Composition.Laws NaturalTransformation.Paths