--- a/state/state.agda	Tue May 03 16:01:54 2016 +0900
+++ b/state/state.agda	Tue May 03 16:31:56 2016 +0900
@@ -2,6 +2,24 @@
 open import Level
 open ≡-Reasoning
 
+
+module state where
+
+record Product {l : Level} (A B : Set l) : Set (suc l) where 
+  constructor <_,_>
+  field
+    first  : A
+    second : B
+open Product
+
+id : {l : Level} {A : Set l} -> A -> A
+id a = a
+
+
+infixr 10 _∘_
+_∘_ : {l : Level} {A B C : Set l} -> (B -> C) -> (A -> B) -> (A -> C)
+g ∘ f = \a -> g (f a)
+
 {-
 Haskell Definition
 newtype State s a = State { runState :: s -> (a, s) }
@@ -13,14 +31,6 @@
     in runState (k a) s'
 -}
 
-module state where
-
-record Product {l : Level} (A B : Set l) : Set (suc l) where 
-  constructor <_,_>
-  field
-    first  : A
-    second : B
-open Product
 
 record State {l : Level} (S A : Set l) : Set (suc l) where
   field
@@ -30,8 +40,26 @@
 state : {l : Level} {S A : Set l} -> (S -> Product A S) -> State S A
 state f = record {runState = f}
 
-return : {l : Level} {S A : Set l}  -> A -> State S A
+return : {l : Level} {S A : Set l} -> A -> State S A
 return a = state (\s -> < a , s > )
 
 _>>=_ : {l : Level} {S A B : Set l} -> State S A -> (A -> State S B) -> State S B
-m  >>= k =  state (\s -> (State.runState (k (Product.first (State.runState m s))) (Product.second (State.runState m s))))
\ No newline at end of file
+m  >>= k =  state (\s -> (runState (k (first (runState m s))) (second (runState m s))))
+
+{- fmap definitions in Haskell
+instance Functor (State s) where
+    fmap f m = State $ \s -> let
+        (a, s') = runState m s
+        in (f a, s')
+-}
+
+fmap : {l : Level} {S A B : Set l} -> (A -> B) -> (State S A) -> (State S B)
+fmap f m = state (\s -> < (f (first ((runState m) s))), (second ((runState m) s)) >)
+
+-- proofs
+
+fmap-id : {l : Level} {A S : Set l} {s : State S A} -> fmap id s ≡ id s
+fmap-id = refl
+
+fmap-comp : {l : Level} {S A B C : Set l} {g : B -> C} {f : A -> B} {s : State S A} ->  ((fmap g) ∘ (fmap f)) s ≡ fmap (g ∘ f) s
+fmap-comp {_}{_}{_}{_}{_}{g}{f}{s} = refl