Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 36:169ec60fcd36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof Monad-law-4
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 14:22:34 +0900
parents c5cdbedc68ad
children 6ce83b2c9e59
comparison
equal deleted inserted replaced
35:c5cdbedc68ad 36:169ec60fcd36
50 ∎ 50 ∎
51 51
52 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Similar A) -> (mu ∙ return) s ≡ id s 52 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Similar A) -> (mu ∙ return) s ≡ id s
53 monad-law-2-2 (similar lx x ly y) = refl 53 monad-law-2-2 (similar lx x ly y) = refl
54 54
55 {-
56 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return
57 monad-law-3 = {!!}
58 55
59 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu 56 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (return ∙ f) x ≡ (fmap f ∙ return) x
60 monad-law-4 = {!!} 57 monad-law-3 f x = refl
61 -} 58
59
60 monad-law-4 : {l : Level} {A B : Set l} (f : A -> B) (s : Similar (Similar A)) ->
61 (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s
62 monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl