§ Monadic functor
- A fuctor is monadic iff it has a left adjoint and the adjunction is monadic.
- An adjunction is monadic if the induced "comparison functor" from to the category of algebras (eilenberg-moore category) is an equivalence of categories .
- That is, the functor is an equivalence of categories.
- Some notes: We have and not the other way around since the full order is : Kleisli, to , to Eilenberg moore. We go from "more semantics" to "less semantics" --- such induced functors cannot "add structure" (by increasing the amount of semantics), but they can "embed" more semantics into less semantics. Thus, there is a comparison functor from to .
- Eilenberg-moore is written since the category consists of -algebras, where is the induced monad . It's because a algebra consists of arrows with some laws. If one wished to be cute, the could think of this as " ".
- The monad is and not because, well, let's pick a concrete example:
Mon. The monad on the set side takes a set to the set of words on , written . The other alleged "monad" takes a monoid to the free monoid on the element of . We've lost structure.