Commit 2025-09-17 08:13 6845e572

feat(CategoryTheory/Bicategory/Functor): strictly unitary lax/pseudo functors (#27849) We define strictly unitary lax/pseudo functors between bicategories. A lax (resp. pseudo-)functor from C to D is strictly unitary if F.map(𝟙 X) = 𝟙 (F.obj X) and if the 2-cell mapId is the identity 2-cell induced by this equality. We provide a constructor for those that do not require the mapId field. Although this structure is somewhat "evil" from a purely categorical perspective (it mentions non-definitonal equality of objects in a 1-category), these class of functors are of interest: strictly unitary lax functors are part of the definition of the Duskin nerve of a bicategory (which embeds bicategories in the theory of simplicial sets), while strictly unitary pseudofunctors are part of the definition of the 2-nerve of a bicategory, which embeds bicategories into the theory of simplicial categories. This PR is part of an ongoing work that will hopefully culminate with the construction of the Duskin Nerve, as well as a proof of the fact that the Duskin nerve of a locally groupoidal bicategory is a quasicategory.