Theorem CategoryTheory.StrictlyUnitaryLaxFunctor.comp_id

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