From 3e123312948402504f8d3a6c7b0dc7ace1c518de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 14:01:57 +0100
Subject: [PATCH] Monoidal monads addendum

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

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 0400ba1..46d0073 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -71,6 +71,12 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       isAssociative : IsAssociative
       isInverse : IsInverse
 
+  record Monad : Set ℓ where
+    field
+      raw : RawMonad
+      isMonad : IsMonad raw
+    open IsMonad isMonad public
+
 -- "A monad in the Kleisli form" [vlad]
 module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private