Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 35:c5cdbedc68ad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof Monad-law-2-2
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 14:15:13 +0900
parents b7c4e6276bcf
children 169ec60fcd36
comparison
equal deleted inserted replaced
34:b7c4e6276bcf 35:c5cdbedc68ad
47 similar lx x (ly ++ []) y 47 similar lx x (ly ++ []) y
48 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩ 48 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩
49 similar lx x ly y 49 similar lx x ly y
50 ∎ 50 ∎
51 51
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
54
52 {- 55 {-
53 monad-law-2-2 : mu ∙ return ≡ id
54 monad-law-2-2 = {!!}
55
56 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return 56 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return
57 monad-law-3 = {!!} 57 monad-law-3 = {!!}
58 58
59 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu 59 monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu
60 monad-law-4 = {!!} 60 monad-law-4 = {!!}