PreCategory := (pseudofunctor_of_functor_to_cat F).
Require Import Category.Core Functor.Core. Require Import Pseudofunctor.FromFunctor. Require Import Cat.Core. Require Import Grothendieck.PseudofunctorToCat.