Commit 2024-10-25 15:10 533ce927
View on Github →feat(CategoryTheory): constructor for pseudofunctors from a strict locally discrete category (#18201)
In this file, we define a constructor pseudofunctorOfIsLocallyDiscrete for the type Pseudofunctor B C when C is any bicategory, and B is a strict locally discrete category. Indeed, in this situation, we do not need to care about the field map₂ of pseudofunctors because all the 2-morphisms in B are identities.