PreCategory := @Build_PreCategory { C : PreCategory | P C } (fun C D => Functor C.
Require Import Category.Objects InitialTerminalCategory.Core InitialTerminalCategory.Functors Functor.Core Category.Strict Functor.Paths. Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Laws.