diff agda/laws.agda @ 94:bcd4fe52a504

Rewrite monad definitions for delta/deltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 17:10:29 +0900
parents 55d11ce7e223
children f26a954cd068
line wrap: on
line diff
--- a/agda/laws.agda	Mon Jan 19 15:21:29 2015 +0900
+++ b/agda/laws.agda	Mon Jan 19 17:10:29 2015 +0900
@@ -32,12 +32,15 @@
                          (M : {ll : Level} -> Set ll -> Set ll)
                          (functorM : Functor M)
                          : Set (suc l)  where
-  field
-    mu  : {A : Set l} -> M (M A) -> M A
-    eta : {A : Set l} -> A -> M A
-  field
+  field -- category
+    mu  :  {A : Set l} -> M (M A) -> M A
+    eta :  {A : Set l} -> A -> M A
+  field -- haskell
+    return : {A : Set l} -> A -> M A
+    bind   : {A B : Set l} -> M A -> (A -> (M B)) -> M B
+  field -- category laws
     association-law : (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
     left-unity-law  : (x : M A) -> (mu  ∙ (fmap functorM eta)) x ≡ id x
     right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x
 
-open Monad
\ No newline at end of file
+open Monad