Def CategoryTheory.Bicategory.Comonad.toOplax

Modification history

2025-06-06 07:38

Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

feat(CategoryTheory/Bicategory): define bicategory of comonads (#25461)

Added CategoryTheory.Bicategory.Comonad.toOplax View on Github →