Commit 2023-03-24 13:50 951fdcff

View on Github →

feat: port CategoryTheory.Monad.Basic (#2969)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monad/Basic.lean

added def CategoryTheory.Comonad.Simps.coe

added def CategoryTheory.Comonad.Simps.δ

added def CategoryTheory.Comonad.Simps.ε

added theorem CategoryTheory.Comonad.coassoc

added def CategoryTheory.Comonad.id

added theorem CategoryTheory.Comonad.left_counit

added theorem CategoryTheory.Comonad.right_counit

added def CategoryTheory.Comonad.δ

added def CategoryTheory.Comonad.ε

added structure CategoryTheory.Comonad

added theorem CategoryTheory.ComonadHom.ext'

added theorem CategoryTheory.ComonadHom.id_toNatTrans

added structure CategoryTheory.ComonadHom

added def CategoryTheory.ComonadIso.mk

added def CategoryTheory.ComonadIso.toNatIso

added def CategoryTheory.Monad.Simps.coe

added def CategoryTheory.Monad.Simps.η

added def CategoryTheory.Monad.Simps.μ

added theorem CategoryTheory.Monad.assoc

added def CategoryTheory.Monad.id

added theorem CategoryTheory.Monad.left_unit

added theorem CategoryTheory.Monad.right_unit

added def CategoryTheory.Monad.η

added def CategoryTheory.Monad.μ

added structure CategoryTheory.Monad

added theorem CategoryTheory.MonadHom.comp_toNatTrans

added theorem CategoryTheory.MonadHom.ext'

added theorem CategoryTheory.MonadHom.id_toNatTrans

added structure CategoryTheory.MonadHom

added def CategoryTheory.MonadIso.mk

added def CategoryTheory.MonadIso.toNatIso

added def CategoryTheory.comonadToFunctor

added theorem CategoryTheory.comonadToFunctor_mapIso_comonad_iso_mk

added theorem CategoryTheory.comp_toNatTrans

added def CategoryTheory.monadToFunctor

added theorem CategoryTheory.monadToFunctor_mapIso_monad_iso_mk