Structure CategoryTheory.StrictlyUnitaryLaxFunctor

Modification history

2025-11-05 18:48
Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean
chore(Bicategory/Functor): add notation for lax and oplax functors (#31238) …
Modified CategoryTheory.StrictlyUnitaryLaxFunctorView on Github →
2025-09-17 08:13
Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean
feat(CategoryTheory/Bicategory/Functor): strictly unitary lax/pseudo functors (#27849) …
Added CategoryTheory.StrictlyUnitaryLaxFunctorView on Github →