context | C … category |
definiendum | ⟨T,η,μ⟩ in it |
inclusion | T in CC |
inclusion | η:1C∙→T |
inclusion | μ:TT∙→T |
postulate | μ∘Tμ=μ∘μT |
postulate | μ∘Tη=μ∘ηT=1T |
A monad is functor together with two natural transformations that fulfill some algebraic relations.
Written out in component form, the postulates read
Picture the following chain of objects and notice that the axioms merely say the following: All ways ending up at TX must be the same.
XηX→TXT(ηTX) or ηTX→ μX←TTXT(μX) or μTX←TTTX
All monads arise by transferring some co-unit into the other category: Set T:=GF and μY:=G(εFY) and you got yourself a monad ⟨T,η,μ⟩.
The forward arrows ηX are called „unit“ or, in programmer circles, „return“. The backwards arrows μX are called „join“ and from the counit-unit adjunction perspective, they are the arrow images of the functor applied to the „co-unit“ components.
Recall that Set can be equipped with a monoidal structure where units are singletons (= final objects in Set, e.g. 1:={0}) and the product ⊗ can be taken to be the Cartesian product M⊗N:=M×N (= categorical product for Set). Here, a monoid object is a triple given by
M,
e:1→M,
∗:M×M→M.
Now a monad is given by
T,
η:1C∙→T,
μ:TT∙→T
and is also a monoid object, namely in the category of endofunctors CC, with the monoidal product ⊗ (not the categorical product) given by concatenation of functors S⊗T:=ST.
Wikipedia: Monad (category theory), Monade (Informatik)