Mercurial > hg > Members > kono > Proof > category

changeset 102:09af60198ce5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on goning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 15:26:25 +0900
parents 0f7086b6a1a6
children 8dcf926482af
files em-category.agda
diffstat 1 files changed, 5 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Wed Jul 31 15:17:15 2013 +0900
+++ b/em-category.agda	Wed Jul 31 15:26:25 2013 +0900
@@ -31,22 +31,19 @@
 --
 open Functor
 open NTrans
-record IsEMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
-     (a : Obj A)  (φ  : Hom A (FObj T a) a ) : Set c₁ where
+record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
    field
        identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
        eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
 open IsEMAlgebra
 
-record EMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
-     (a : Obj A)  (φ  : FObj T a -> a ) : Set  c₂ where
+record EMAlgebra (a : Obj A)  (φ : Hom A (FObj T a) a ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ))  where
   field
-     isEMAlbgebra : IsEMAlgebra {c₁} {c₂} {ℓ} {A} {T} a φ 
+     isEMAlbgebra : IsEMAlgebra a φ 
 open EMAlgebra
      
-data EMObj { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
-     {a : Obj A}  {φ  : FObj T a -> a } {EMAlgebra a φ} : Set ( c₁ ⊔ c₂ ) where
-            emObj : \a φ -> (IsEMAlgebra a φ) -> EMObj { c₁} {c₂} {ℓ} {A} {T} {a} {φ}
+data EMObj {a : Obj A}  {φ  : Hom A (FObj T a) a }  : Set ( c₁ ⊔ c₂ ) where
+            emObj : \a φ -> (IsEMAlgebra a φ) -> EMObj {a} {φ}
 
 emobj : EMObj -> Obj A
 emobj (emObj x φ isAlgebra) = x