The Coq mailing list

[ahrens <Benedikt.Ahrens AT unice.fr>]

On 02/18/2011 06:21 PM, AUGER Cedric wrote:
> Hi all.
> 
> I wanted to learn what is a monad, so I read some tutorial on it and
> wrote this implementation in Coq
> (http://coq.inria.fr/cocorico/AUGER_Monad).

I have implemented monads and relative monads over arbitrary categories
(resp. arbitrary functors for relative monads) as well as their
morphisms and some examples (abstract syntax, mainly) in Coq.
However, if you are only interested in monads on Type, it might be of
little interest for you since its generality may make it more cumbersome
to use.

You can find links to the repo and online documentation at
http://math.unice.fr/~ahrens/#work

Greetings
ben