Cat-valued pseudofunctors

Extensions of Mathlib's CategoryTheory/Bicategory/Functor/Cat/, where Pseudofunctor.ObjectProperty is defined: replete and restriction-stable fiberwise loci with their full subpseudofunctors, and transport of a Cat-valued pseudofunctor presentation through objectwise equivalences. Declarations use Mathlib's CategoryTheory.Pseudofunctor namespace.