Mercurial > hg > Members > atton > delta_monad
comparison agda/similar.agda @ 30:c2f40b6d4027
Expand monad-law-1
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Oct 2014 15:32:11 +0900 |
parents | e0ba1bf564dd |
children | 71906644d206 |
comparison
equal
deleted
inserted
replaced
29:e0ba1bf564dd | 30:c2f40b6d4027 |
---|---|
25 returnSS : {A : Set} -> A -> A -> Similar A | 25 returnSS : {A : Set} -> A -> A -> Similar A |
26 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y | 26 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y |
27 | 27 |
28 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu | 28 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu |
29 | 29 |
30 {- | |
30 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s) | 31 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s) |
31 monad-law-1 s = begin | 32 monad-law-1 s = begin |
32 ((mu ∙ (fmap mu)) s) | 33 ((mu ∙ (fmap mu)) s) |
33 ≡⟨⟩ | 34 ≡⟨⟩ |
34 mu (fmap mu s) | 35 mu (fmap mu s) |
35 ≡⟨ {!!} ⟩ | 36 ≡⟨ cong mu {!!} ⟩ |
36 mu (mu s) | 37 mu (mu s) |
37 ≡⟨⟩ | 38 ≡⟨⟩ |
38 ((mu ∙ mu) s) | 39 ((mu ∙ mu) s) |
39 ∎ | 40 ∎ |
41 -} | |
42 | |
43 monad-law-1-sub : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> fmap mu s ≡ mu s | |
44 monad-law-1-sub (similar lx (similar llx (similar lllx x _ _) _ _) ly (similar _ _ lly (similar _ _ llly y))) = begin | |
45 similar lx (mu (similar llx (similar lllx x _ _) _ _)) ly | |
46 (mu (similar _ _ lly (similar _ _ llly y))) | |
47 ≡⟨ {!!} ⟩ | |
48 similar (lx ++ llx) (similar lllx x _ _) (ly ++ lly) | |
49 (similar _ _ llly y) | |
50 ∎ | |
51 | |
40 | 52 |
41 | 53 |
42 | 54 |
43 | 55 |
44 {- | 56 {- |