Mercurial > hg > Members > atton > similar_monad
changeset 34:b7c4e6276bcf
Proof Monad-law-2-1
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Oct 2014 14:13:00 +0900 |
| parents | 0bc402f970b3 |
| children | c5cdbedc68ad |
| files | agda/similar.agda |
| diffstat | 1 files changed, 13 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/similar.agda Sat Oct 18 14:04:33 2014 +0900 +++ b/agda/similar.agda Sat Oct 18 14:13:00 2014 +0900 @@ -16,7 +16,7 @@ mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y -return : {A : Set} -> A -> Similar A +return : {l : Level} {A : Set l} -> A -> Similar A return x = similar [] x [] x returnS : {A : Set} -> A -> Similar A @@ -37,11 +37,19 @@ similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y ∎ + +--monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡ id +monad-law-2-1 : {l : Level} {A : Set l} -> (s : Similar A) -> + (mu ∙ fmap return) s ≡ (mu ∙ return) s +monad-law-2-1 (similar lx x ly y) = begin + similar (lx ++ []) x (ly ++ []) y + ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩ + similar lx x (ly ++ []) y + ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩ + similar lx x ly y + ∎ + {- ---monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id -monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return -monad-law-2-1 = {!!} - monad-law-2-2 : mu ∙ return ≡ id monad-law-2-2 = {!!}