From b6457a0b145a37b6e15365f921fcd65c5002284c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 6 Mar 2018 09:41:29 +0100
Subject: [PATCH] Add comment

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

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 701c986..674fd95 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -28,6 +28,8 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       pureNT : NaturalTransformation F.identity R
       joinNT : NaturalTransformation F[ R ∘ R ] R
 
+    -- Note that `pureT` and `joinT` differs from their definition in the
+    -- kleisli formulation only by having an explicit parameter.
     pureT : Transformation F.identity R
     pureT = proj₁ pureNT
     pureN : Natural F.identity R pureT