# mathlibdocumentation

We define bundled (co)monads as a structure consisting of a functor func : C ⥤ C endowed with a term of type (co)monad func. See category_theory.monad.basic for the definition. The type of bundled (co)monads on a category C is denoted (Co)Monad C.

We also define morphisms of bundled (co)monads as morphisms of their underlying (co)monads in the sense of category_theory.(co)monad_hom. We construct a category instance on (Co)Monad C.

structure category_theory.Monad (C : Type u)  :
Type (max u v)
• func : C C
• str : . "apply_instance"

structure category_theory.Comonad (C : Type u)  :
Type (max u v)
• func : C C
• str : . "apply_instance"

def category_theory.Monad.initial (C : Type u)  :

The initial monad. TODO: Prove it's initial.

Equations
@[instance]
def category_theory.Monad.inhabited {C : Type u}  :

Equations
@[instance]

Equations
def category_theory.Monad.hom {C : Type u} (M N : category_theory.Monad C) :
Type (max u v)

Morphisms of bundled monads.

Equations
@[instance]

Equations
@[instance]

Equations
def category_theory.Monad.forget (C : Type u)  :
C C

The forgetful functor from Monad C to C ⥤ C.

Equations
@[simp]
theorem category_theory.Monad.comp_to_nat_trans {C : Type u} {M N L : category_theory.Monad C} (f : M N) (g : N L) :

@[simp]
theorem category_theory.Monad.assoc_func_app {C : Type u} {M : category_theory.Monad C} {X : C} :
M.func.map ((μ_ M.func).app X) (μ_ M.func).app X = (μ_ M.func).app (M.func.obj X) (μ_ M.func).app X

def category_theory.Comonad.terminal (C : Type u)  :

The terminal comonad. TODO: Prove it's terminal.

Equations
@[instance]
def category_theory.Comonad.inhabited {C : Type u}  :

Equations
@[instance]

Equations
def category_theory.Comonad.hom {C : Type u} (M N : category_theory.Comonad C) :
Type (max u v)

Morphisms of bundled comonads.

Equations
@[instance]

Equations
def category_theory.Comonad.forget (C : Type u)  :

The forgetful functor from CoMonad C to C ⥤ C.

Equations
@[simp]
theorem category_theory.Comonad.comp_to_nat_trans {C : Type u} {M N L : category_theory.Comonad C} (f : M N) (g : N L) :

@[simp]
theorem category_theory.Comonad.coassoc_func_app {C : Type u} {M : category_theory.Comonad C} {X : C} :
(δ_ M.func).app X M.func.map ((δ_ M.func).app X) = (δ_ M.func).app X (δ_ M.func).app (M.func.obj X)