Def CategoryTheory.StrictlyUnitaryLaxFunctor.mk'

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.StrictlyUnitaryLaxFunctor.mk'View on Github →