Mercurial > hg > Members > atton > delta_monad

diff agda/laws.agda @ 102:9c62373bd474

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 25 Jan 2015 12:16:34 +0900
parents f26a954cd068
children a271f3ff1922
line wrap: on
line diff
--- a/agda/laws.agda	Sun Jan 25 12:15:19 2015 +0900
+++ b/agda/laws.agda	Sun Jan 25 12:16:34 2015 +0900
@@ -43,5 +43,8 @@
     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
+  field -- natural transformations
+    eta-is-nt : {B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x)
+
 
 open Monad
\ No newline at end of file