Mercurial > hg > Members > kono > Proof > category

changeset 132:683d4e590762

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
trying..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2013 15:54:09 +0900
parents eb7ca6b9d327
children 731e00f31f4f
files monoid-monad.agda
diffstat 1 files changed, 10 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Sun Aug 11 15:52:09 2013 +0900
+++ b/monoid-monad.agda	Sun Aug 11 15:54:09 2013 +0900
@@ -13,26 +13,23 @@
 --    a -> m x a
 --    m x a -> m' x (m x a)
 
-data T1 {c₁ c₂ ℓ : Level}  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( suc ( c₁ ⊔ c₂ ⊔ ℓ) ) where
+data T1  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( suc ( c₁ ⊔ c₂ ⊔ ℓ) ) where
    T1a :  Obj A -> T1 M A
    T1t :  Obj A -> T1 M A -> T1 M A
 
-T1HomMap : {c₁ c₂ ℓ : Level}  { A : Category c₁ c₂ ℓ }  {M :  Monoid c₁ ℓ }  (a : T1 {c₁} {c₂} {ℓ} M A ) (b : T1  {c₁} {c₂} {ℓ} M A) -> Set c₂ 
-T1HomMap {c₁} {c₂} {ℓ }  { A } (T1a a1 ) (T1a a2 ) = Hom A a1 a2
-T1HomMap {c₁} {c₂} {ℓ }  { A } (T1t a1 t1 ) (T1a a2 ) = Hom A a1 a2
-T1HomMap {c₁} {c₂} {ℓ }  { A } (T1a a1 ) (T1t a2 t2 ) = Hom A a1 a2
-T1HomMap {c₁} {c₂} {ℓ }  { A } (T1t a1 t1 ) (T1t a2 t2 ) = Hom A a1 a2
+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
 
-record T1Hom1 {c₁ c₂ ℓ : Level}  { M : Monoid  c₁  ℓ}  { A : Category c₁ c₂ ℓ }  
-                 (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
 
-open T1Hom1
-T1Hom = \(a b : T1 M A) -> T1Hom1 {c₁} {c₂} {ℓ} {M} {A} a b
-
-_*_ :  {c₁ c₂ ℓ : Level}  { A : Category c₁ c₂ ℓ }  {M :  Monoid c₁ ℓ } { a b c : T1 {c₁} {c₂} {ℓ } M A } -> T1Hom1  {c₁} {c₂} {ℓ} b c -> T1Hom1  {c₁} {c₂} {ℓ} a b -> T1Hom1  {c₁} {c₂} {ℓ} a c
-_*_ {c₁} {c₂} {ℓ } {A} {M} {a} {b} {c} g f  =  record { T1Map = A [ T1Map g  o T1Map f ] } 
+open T1Hom
+_*_ :  { a b c : T1 M A } -> T1Hom b c -> T1Hom a b -> T1Hom  a c
+_*_  g f  =  record { T1Map = A [ T1Map g  o T1Map f ] }