Mercurial > hg > Members > kono > Proof > category

changeset 133:731e00f31f4f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hom composition passed.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2013 16:11:55 +0900
parents 683d4e590762
children de1c3443f10d
files monoid-monad.agda
diffstat 1 files changed, 6 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- 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