--- a/free-monoid.agda	Sun Aug 18 21:30:00 2013 +0900
+++ b/free-monoid.agda	Sun Aug 18 22:17:46 2013 +0900
@@ -12,17 +12,15 @@
 open import  Relation.Binary.PropositionalEquality
 
 
-A = Sets {c₁}
-B = CAT  
 
 infixr 40 _::_
-data  List  (A : Set ) : Set  where
+data  List  (A : Set c ) : Set c where
    [] : List A
    _::_ : A -> List A -> List A
 
 
 infixl 30 _++_
-_++_ :   {A : Set } -> List A -> List A -> List A
+_++_ :   {A : Set c } -> List A -> List A -> List A
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
@@ -31,46 +29,30 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
-isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_  _++_  []
-isListCategory  A = record  { isEquivalence =  isEquivalence1 {A}
-                    ; identityL =   list-id-l
-                    ; identityR =   list-id-r
-                    ; o-resp-≈ =    o-resp-≈ {A}
-                    ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
-                    }
-     where
-        list-id-l : { A : Set } -> { x : List A } ->  [] ++ x ≡ x
-        list-id-l {_} {_} = refl
-        list-id-r : { A : Set } -> { x : List A } ->  x ++ [] ≡ x
-        list-id-r {_} {[]} =   refl
-        list-id-r {A} {x :: xs} =  ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) 
-        list-assoc : {A : Set} -> { xs ys zs : List A } ->
-              ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
-        list-assoc  {_} {[]} {_} {_} = refl
-        list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( \y  -> x :: y ) 
-                 ( list-assoc {A} {xs} {ys} {zs} )
-        o-resp-≈ :  {A : Set} ->  {f g : List A } → {h i : List A } → 
-                          f ≡  g → h ≡  i → (h ++ f) ≡  (i ++ g)
-        o-resp-≈  {A} refl refl = refl
-        isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A }  _≡_ 
-        isEquivalence1 {A} =      -- this is the same function as A's equivalence but has different types
-           record { refl  = refl
-             ; sym   = sym
-             ; trans = trans
-             } 
-ListCategory : (A : Set) -> Category _ _ _
-ListCategory A =
-  record { Obj = ListObj
-         ; Hom = \a b -> List  A
-         ; _o_ = _++_ 
-         ; _≈_ = _≡_
-         ; Id  =  []
-         ; isCategory = ( isListCategory A )
-          }
+list-id-l : { A : Set c } -> { x : List A } ->  [] ++ x ≡ x
+list-id-l {_} {_} = refl
+list-id-r : { A : Set c } -> { x : List A } ->  x ++ [] ≡ x
+list-id-r {_} {[]} =   refl
+list-id-r {A} {x :: xs} =  ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) 
+list-assoc : {A : Set c} -> { xs ys zs : List A } ->
+      ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
+list-assoc  {_} {[]} {_} {_} = refl
+list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( \y  -> x :: y ) 
+         ( list-assoc {A} {xs} {ys} {zs} )
+list-o-resp-≈ :  {A : Set c} ->  {f g : List A } → {h i : List A } → 
+                  f ≡  g → h ≡  i → (h ++ f) ≡  (i ++ g)
+list-o-resp-≈  {A} refl refl = refl
+list-isEquivalence : {A : Set c} -> IsEquivalence {_} {_} {List A }  _≡_ 
+list-isEquivalence {A} =      -- this is the same function as A's equivalence but has different types
+   record { refl  = refl
+     ; sym   = sym
+     ; trans = trans
+     } 
 
 open import Algebra.FunctionProperties using (Op₁; Op₂)
+open import Algebra.Structures
+open import Data.Product
 
-open import Algebra.Structures
 
 record ≡-Monoid : Set (suc c) where
   infixl 7 _∙_
@@ -82,6 +64,22 @@
 
 open ≡-Monoid
 
+list  : (a : Set c) -> ≡-Monoid
+list a = record {
+    Carrier    =  List a
+    ; _∙_      = _++_
+    ; ε        = []
+    ; isMonoid = record {
+          identity = ( ( \x -> list-id-l {a}  ) , ( \x -> list-id-r {a} ) ) ;
+          isSemigroup = record {
+               assoc =  \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} )
+             ; isEquivalence = list-isEquivalence
+             ; ∙-cong = \x -> \y ->  list-o-resp-≈ y x
+          }
+      }
+    }
+
+
 record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
   field
       morph : Carrier a -> Carrier b  
@@ -139,24 +137,24 @@
            }
 
 
-
+A = Sets {c}
+B = MonoidCategory  
 
--- open Functor
+open Functor
 
--- U : Functor B A
--- U = record {
---        FObj = \c -> Obj c ;
---        FMap = \f -> (\x -> FMap f x) ;
---        isFunctor = record {
---               ≈-cong   = ≈-cong
---              ; identity = identity1
---              ; distr    = distr1
---        }
---    } where
---         identity1 : {a : Obj B} →  A [ FMap identityFunctor ≈ ( \x -> x ) ]
---         identity1 {a} = _≡_.refl
---         ≈-cong : {a b : Obj B} {f g : Hom B a b} → B [ f ≈ g ] → ?
---         ≈-cong {a} {b} {f} {g}   = ?
---         distr1 :  {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} →  A [ ( FMap ( g ○  f )) ≈  ( \x -> FMap g (FMap f x ))  ]
---         distr1 {a} {b} {c} {f} {g} = ?
+U : Functor B A
+U = record {
+       FObj = \m -> Carrier m ;
+       FMap = \f -> morph f ;
+       isFunctor = record {
+              ≈-cong   = \x -> x
+             ; identity = refl
+             ; distr    = refl
+       }
+   } 
 
+-- FObj 
+
+Generator : Obj A -> Obj B
+Generator s =  list s
+