Commit 2025-06-06 07:38 dd260672

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Bicategory/End.lean

deleted def CategoryTheory.EndMonoidal

Modified Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean

added theorem CategoryTheory.OplaxFunctor.mapComp_id_left

added theorem CategoryTheory.OplaxFunctor.mapComp_id_right

Created Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

added theorem CategoryTheory.Bicategory.Comonad.comul_assoc

added theorem CategoryTheory.Bicategory.Comonad.comul_assoc_flip

added theorem CategoryTheory.Bicategory.Comonad.comul_counit

added theorem CategoryTheory.Bicategory.Comonad.counit_comul

added def CategoryTheory.Bicategory.Comonad.ofOplaxFromUnit

added def CategoryTheory.Bicategory.Comonad.toOplax

added def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.hom

added def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad

added theorem CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_comul

added theorem CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_counit

added theorem CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_hom

added def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.obj

added def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.toOplax

added def CategoryTheory.Bicategory.OplaxTrans.ComonadBicat

Modified Mathlib/CategoryTheory/Bicategory/SingleObj.lean

modified def CategoryTheory.MonoidalSingleObj