2025-09-17 08:13
Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean
feat(CategoryTheory/Bicategory/Functor): strictly unitary lax/pseudo functors (#27849) …
Added CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp