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 = {!!}