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 {-