Theorem CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv

Modification history

2025-06-16 07:03
Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean
feat(CategoryTheory): pseudofunctors from strict bicategories (#24382) …
Added CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_invView on Github →