Def CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso

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