Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.agda @ 122:e1900c89dea9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix Monad-proof for Delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 12:12:14 +0900
parents e6bcc7467335
children d205ff1e406f
comparison
equal deleted inserted replaced
121:673e1ca0d1a9 122:e1900c89dea9
142 142
143 143
144 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor 144 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor
145 delta-is-monad = record { eta = delta-eta; 145 delta-is-monad = record { eta = delta-eta;
146 mu = delta-mu; 146 mu = delta-mu;
147 return = delta-eta;
148 bind = delta-bind;
149 eta-is-nt = delta-eta-is-nt; 147 eta-is-nt = delta-eta-is-nt;
150 mu-is-nt = delta-mu-is-nt; 148 mu-is-nt = delta-mu-is-nt;
151 association-law = monad-law-1; 149 association-law = monad-law-1;
152 left-unity-law = delta-left-unity-law ; 150 left-unity-law = delta-left-unity-law ;
153 right-unity-law = \x -> (sym (delta-right-unity-law x)) } 151 right-unity-law = \x -> (sym (delta-right-unity-law x)) }