# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1413701635 -32400
# Node ID 6ce83b2c9e596e4224498a999f150b1f1b3e1f53
# Parent  743c05b98dad324cc31fa1be8d42a4bfe4f90cf7
Proof Functor-laws

diff -r 743c05b98dad -r 6ce83b2c9e59 agda/similar.agda
--- a/agda/similar.agda	Sun Oct 19 12:22:54 2014 +0900
+++ b/agda/similar.agda	Sun Oct 19 15:53:55 2014 +0900
@@ -10,22 +10,46 @@
 data Similar {l : Level} (A : Set l) : (Set (suc l)) where
   similar : List String -> A -> List String -> A -> Similar A
 
+
+-- Functor
 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Similar A) -> (Similar B)
 fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
 
+
+-- Monad
 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 : {l : Level} {A : Set l} -> A -> Similar A
 return x = similar [] x [] x
 
-returnS : {A : Set} -> A -> Similar A
+returnS : {l : Level} {A : Set l} -> A -> Similar A
 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
 
-returnSS : {A : Set} -> A -> A -> Similar A
+returnSS : {l : Level} {A : Set l} -> A -> A -> Similar A
 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
 
 
+
+-- proofs
+
+
+-- Functor-laws
+
+-- Functor-law-1 : T(id) = id'
+functor-law-1 :  {l : Level} {A : Set l} ->  (s : Similar A) -> (fmap id) s ≡ id s
+functor-law-1 (similar lx x ly y) = refl
+
+-- Functor-law-2 : T(f . g) = T(f) . T(g)
+functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
+                (f : B -> C) -> (g : A -> B) -> (s : Similar A) ->
+                (fmap (f ∙ g)) s ≡ ((fmap f) ∙ (fmap g)) s
+functor-law-2 f g (similar lx x ly y) = refl
+
+
+
+-- Monad-laws
+
 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _))