Theorem CategoryTheory.StrictlyUnitaryLaxFunctor.id_comp

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