From 7cddba97a85f83d360174b2ae070513ec01c5fdb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 19:03:30 +0100
Subject: [PATCH] Shorten definition

---
 src/Cat/Category/Monad.agda | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 92805e0..9b80df3 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -35,19 +35,13 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
     private
       module R  = Functor R
-      module RR = Functor F[ R ∘ R ]
-      module _ {X : Object} where
-        IsAssociative' : Set _
-        IsAssociative' = μ X ∘ R.func→ (μ X) ≡ μ X ∘ μ (R.func* X)
-        IsInverse' : Set _
-        IsInverse'
-          = μ X ∘ η (R.func* X) ≡ 𝟙
-          × μ X ∘ R.func→ (η X) ≡ 𝟙
-
-    -- We don't want the objects to be indexes of the type, but rather just
-    -- universally quantify over *all* objects of the category.
-    IsAssociative = {X : Object} → IsAssociative' {X}
-    IsInverse = {X : Object} → IsInverse' {X}
+    IsAssociative : Set _
+    IsAssociative = {X : Object}
+      → μ X ∘ R.func→ (μ X) ≡ μ X ∘ μ (R.func* X)
+    IsInverse : Set _
+    IsInverse = {X : Object}
+      → μ X ∘ η (R.func* X) ≡ 𝟙
+      × μ X ∘ R.func→ (η X) ≡ 𝟙
 
   record IsMonad (raw : RawMonad) : Set ℓ where
     open RawMonad raw public