Def CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor

Modification history

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 View on Github →