Cosmetics

src/Cat/Category/Monad.agda

@@ -21,6 +21,7 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   open NaturalTransformation ℂ ℂ
   record RawMonad : Set ℓ where
     field
+      -- TODO rename fields here
       -- R ~ m
       R : EndoFunctor ℂ
       -- η ~ pure
@@ -316,8 +317,9 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       Kraw.bind forthRaw = bind
 
     module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
-      module MI = M.IsMonad m
+      private
-      module KI = K.IsMonad
+        module MI = M.IsMonad m
+        module KI = K.IsMonad
       forthIsMonad : K.IsMonad (forthRaw raw)
       KI.isIdentity     forthIsMonad = proj₂ MI.isInverse
       KI.isNatural      forthIsMonad = MI.isNatural
@@ -328,10 +330,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
     Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
 
     module _ (m : K.Monad) where
-      private
+      open K.Monad m
-        module ℂ = Category ℂ
-        open K.Monad m
-        open NaturalTransformation ℂ ℂ
 
       module MR = M.RawMonad
       backRaw : M.RawMonad
@@ -339,13 +338,11 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       MR.ηNatTrans backRaw = ηNatTrans
       MR.μNatTrans backRaw = μNatTrans
 
-    module _ (m : K.Monad) where
+      module MI = M.IsMonad
-      open K.Monad m
+      -- also prove these in K.Monad!
-      open M.RawMonad (backRaw m)
+      backIsMonad : M.IsMonad backRaw
-      module Mis = M.IsMonad
+      MI.isAssociative backIsMonad = {!isAssociative!}
-
+      MI.isInverse backIsMonad = {!!}
-      backIsMonad : M.IsMonad (backRaw m)
-      backIsMonad = {!!}
 
     back : K.Monad → M.Monad
     Monoidal.Monad.raw     (back m) = backRaw     m