--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/list-monoid-cat.agda	Sun Aug 18 19:55:05 2013 +0900
@@ -0,0 +1,115 @@
+open import Category -- https://github.com/konn/category-agda
+open import Level
+open import HomReasoning
+open import cat-utility
+
+module free-monoid (c : Level ) where
+
+postulate A : Set
+
+postulate a : A
+postulate b : A
+
+
+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
+
+open  import  Relation.Binary.Core
+open  import  Relation.Binary.PropositionalEquality
+
+≡-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.Structures
+open import Algebra.FunctionProperties using (Op₁; Op₂)
+
+data MonoidObj : Set c where
+  ! : MonoidObj
+
+record ≡-Monoid c : Set (suc c) where
+  infixl 7 _∙_
+  field
+    Carrier  : Set c
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    isMonoid : IsMonoid _≡_ _∙_ ε
+
+open ≡-Monoid 
+open import Data.Product
+
+isMonoidCategory : (M :  ≡-Monoid c) -> IsCategory MonoidObj (\a b -> Carrier M ) _≡_  (_∙_  M) (ε M)
+isMonoidCategory  M = 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 )
+          }
+
+
+