# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376205115 -32400
# Node ID 731e00f31f4f911655615c7e38d6f20255a8dcfa
# Parent  683d4e590762d099ad88a587ee612488cfc8ea5a
hom composition passed.

diff -r 683d4e590762 -r 731e00f31f4f monoid-monad.agda
--- a/monoid-monad.agda	Sun Aug 11 15:54:09 2013 +0900
+++ b/monoid-monad.agda	Sun Aug 11 16:11:55 2013 +0900
@@ -13,19 +13,17 @@
 --    a -> m x a
 --    m x a -> m' x (m x a)
 
-data T1  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( suc ( c₁ ⊔ c₂ ⊔ ℓ) ) where
+data T1  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( ( c₁ ⊔ c₂ ⊔ ℓ) ) where
    T1a :  Obj A -> T1 M A
    T1t :  Obj A -> T1 M A -> T1 M A
 
-T1HomMap : (a : T1 M A ) (b : T1 M A) -> Set c₂ 
-T1HomMap (T1a a1 ) (T1a a2 ) = Hom A a1 a2
-T1HomMap (T1t a1 t1 ) (T1a a2 ) = Hom A a1 a2
-T1HomMap (T1a a1 ) (T1t a2 t2 ) = Hom A a1 a2
-T1HomMap (T1t a1 t1 ) (T1t a2 t2 ) = Hom A a1 a2
+T1Obj : (a : T1 M A )  -> Obj A
+T1Obj (T1a a1 )  = a1
+T1Obj (T1t a1 t1 )  = a1
 
-record T1Hom (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
+record T1Hom  (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
    field
-       T1Map  : T1HomMap a b
+       T1Map  : Hom A  (T1Obj a) (T1Obj b )
 
 open T1Hom
 _*_ :  { a b c : T1 M A } -> T1Hom b c -> T1Hom a b -> T1Hom  a c