From 8dadfa22a0b02382f9c6015e7311ed515ff99c26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 12 Mar 2018 14:11:31 +0100
Subject: [PATCH] Add documentation header to monad module

---
 src/Cat/Category/Monad.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 257721e..db4e356 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -1,3 +1,21 @@
+{---
+Monads
+
+This module presents two formulations of monads:
+
+  * The standard monoidal presentation
+  * Kleisli's presentation
+
+The first one defines a monad in terms of an endofunctor and two natural
+transformations. The second defines it in terms of a function on objects and a
+pair of arrows.
+
+These two formulations are proven to be equivalent:
+
+    Monoidal.Monad ≃ Kleisli.Monad
+
+ ---}
+
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Category.Monad where