### changeset 121:673e1ca0d1a9

author Yasutaka Higa Mon, 02 Feb 2015 12:11:24 +0900 0f9ecd118a03 e1900c89dea9 agda/laws.agda 1 files changed, 12 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
```--- a/agda/laws.agda	Mon Feb 02 12:07:51 2015 +0900
+++ b/agda/laws.agda	Mon Feb 02 12:11:24 2015 +0900
@@ -13,7 +13,7 @@
-> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x
open Functor

-record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l')
+record NaturalTransformation {l : Level} (F G : Set l -> Set l)
{fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)}
{fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)}
(natural-transformation : {A : Set l}  -> F A -> G A)
@@ -27,23 +27,18 @@

--- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f.
-record Monad {l : Level} (M : Set l -> Set l)
-                         (functorM : Functor M)
-                         : Set (suc l)  where
+record Monad {l : Level} (T : Set l -> Set l) (F : Functor T) : Set (suc l)  where
field -- category
-    mu  :  {A : Set l} -> M (M A) -> M A
-    eta :  {A : Set l} -> A -> M A
-    return : {A : Set l} -> A -> M A
-    bind   : {A B : Set l} -> M A -> (A -> (M B)) -> M B
+    mu  :  {A : Set l} -> T (T A) -> T A
+    eta :  {A : Set l} -> A -> T A
+  field -- natural transformations
+    eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A)       -> (eta ∙ f) x ≡ fmap F f (eta x)
+    mu-is-nt  : {A B : Set l} -> (f : A -> B) -> (x : T (T A)) -> mu (fmap F (fmap F f) x) ≡ fmap F f (mu x)
field -- category laws
-    association-law : {A : Set l} -> (x : (M (M (M A)))) -> (mu ∙ (fmap functorM mu)) x ≡ (mu ∙ mu) x
-    left-unity-law  : {A : Set l} -> (x : M A) -> (mu  ∙ (fmap functorM eta)) x ≡ id x
-    right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x
-  field -- natural transformations
-    eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x)
-    mu-is-nt  : {A B : Set l} -> (f : A -> B) -> (x : M (M A)) -> mu (fmap functorM (fmap functorM f) x) ≡ fmap functorM f (mu x)
+    association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu))  x ≡ (mu ∙ mu) x
+    left-unity-law  : {A : Set l} -> (x : T A)           -> (mu ∙ (fmap F eta)) x ≡ id x
+    right-unity-law : {A : Set l} -> (x : T A)           -> id x ≡ (mu ∙ eta) x