--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/free-monoid.agda	Sun Aug 18 19:55:05 2013 +0900
@@ -0,0 +1,155 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+module free-monoid { c c₁ c₂ ℓ : Level }   where
+
+open import Category.Sets
+open import Category.Cat
+open import HomReasoning
+open import cat-utility
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+
+
+A = Sets {c₁}
+B = CAT  
+
+infixr 40 _::_
+data  List  (A : Set ) : Set  where
+   [] : List A
+   _::_ : A -> List A -> List A
+
+
+infixl 30 _++_
+_++_ :   {A : Set } -> List A -> List A -> List A
+[]        ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+data ListObj : Set where
+  * : ListObj
+
+≡-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 )
+          }
+
+open import Algebra.FunctionProperties using (Op₁; Op₂)
+
+open import Algebra.Structures
+
+record ≡-Monoid : Set (suc c) where
+  infixl 7 _∙_
+  field
+    Carrier  : Set c
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    isMonoid : IsMonoid _≡_ _∙_ ε
+
+open ≡-Monoid
+
+record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
+  field
+      morph : Carrier a -> Carrier b  
+      identity     :  morph (ε a)  ≡  ε b
+      mdistr :  ∀{x y} -> morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )
+
+open Monomorph
+
+_*_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
+_*_ {a} {b} {c} f g =  record {
+      morph = \x ->  morph  f ( morph g x ) ;
+      identity  = identity1 ;
+      mdistr  = mdistr1 
+   } where
+      identity1 : morph f ( morph g (ε a) )  ≡  ε c
+      -- morph f (ε b) = ε c ,  morph g (ε a) ) ≡  ε b
+      -- morph f  morph g (ε a) ) ≡  morph f (ε b) = ε c
+      identity1 = trans ( ≡-cong (morph f ) ( identity g ) )  ( identity f )
+      mdistr1 :  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
+      --  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ morph f ( ( _∙_ c  (morph  g x )) (morph  g y) ) 
+      --  ∀{x y} -> morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
+      mdistr1 = trans  (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) 
+
+
+--isMonoidCategory : IsCategory ≡-Monoid Monomorph _≡_  (_*_  M) (M-id)
+--isMonoidCategory  = ? -- record  { isEquivalence =  isEquivalence1 {M}
+--                     ; identityL =   \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
+--                     ; identityR =   \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
+--                     ; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
+--                     ; o-resp-≈ =    o-resp-≈ {M}
+--                     }
+--      where
+--         o-resp-≈ :  {M :  ≡-Monoid c} ->  {f g : Carrier M } → {h i : Carrier M } → 
+--                           f ≡  g → h ≡  i → (_∙_ M  h f) ≡  (_∙_ M i g)
+--         o-resp-≈  {A} refl refl = refl
+--         isEquivalence1 : {M :  ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M }  _≡_ 
+--         isEquivalence1 {A} =      -- this is the same function as A's equivalence but has different types
+--            record { refl  = refl
+--              ; sym   = sym
+--              ; trans = trans
+--              } 
+-- MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
+-- MonoidCategory M =
+--   record { Obj = MonoidObj
+--          ; Hom = \a b -> Carrier M 
+--          ; _o_ = _∙_  M
+--          ; _≈_ = _≡_
+--          ; Id  =  ε M
+--          ; isCategory = ( isMonoidCategory M )
+--           }
+
+
+
+
+-- 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} = ?
+