Pseudofunctor C := Build_Pseudofunctor C (fun x => pr1 (F x)) (fun s d m => F _1 m) (fun s d d' m0 m1 => Category.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import Functor.Identity. Require Import Pseudofunctor.Core. Require Import Cat.Core. Require Import FunctorCategory.Core. Require Import FunctorCategory.Morphisms NaturalTransformation.Isomorphisms. Require Import Category.Morphisms NaturalTransformation.Paths. Require Import Basics.PathGroupoids Basics.Trunc.