# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375289117 -32400
# Node ID 239fa20251ece12dd6a6200e5e91464d88ac810a
# Parent  5f8d6d1aece451f80e5b6a08e29dfcb590d20424
field version

diff -r 5f8d6d1aece4 -r 239fa20251ec em-category.agda
--- a/em-category.agda	Wed Jul 31 23:53:36 2013 +0900
+++ b/em-category.agda	Thu Aug 01 01:45:17 2013 +0900
@@ -37,40 +37,33 @@
        eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
 open IsEMObj
 
-record EMObj {a : Obj A}  {φ : Hom A (FObj T a) a } : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+record EMObj : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+   field
+       a : Obj A
+       phi : Hom A (FObj T a) a
+       isEMObj : IsEMObj a phi 
    obj : Obj A
    obj = a
-   phi : Hom A (FObj T a) a
-   phi = φ
-   field
-     isEMObj : IsEMObj a φ 
+   φ : Hom A (FObj T a) a
+   φ = phi
 open EMObj
 
 record IsEMHom {x y : Obj A} {φ  : Hom A (FObj T x) x } {φ'  : Hom A (FObj T y) y }
-              (α : Hom A x y) 
-              (a : EMObj {x} {φ}) 
-              (b : EMObj {y} {φ'}) : Set ℓ where
+              (α : Hom A x y) : Set ℓ where
    field
        homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
 open IsEMHom
 
-record Eilenberg-Moore-Hom {x y : Obj A }
-              {φ  : Hom A (FObj T x) x } 
-              {φ' : Hom A (FObj T y) y } 
-              {α : Hom A x y} 
-              (a : EMObj {x} {φ}) 
-              (b : EMObj {y} {φ'}) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
-   EMap    : Hom A x y
-   EMap    = α
+record Eilenberg-Moore-Hom (a : EMObj ) (b : EMObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
    field
-       isEMHom : IsEMHom {x} {y} {φ} {φ'} α a b 
+       EMap    : Hom A (obj a) (obj b)
+       isEMHom : IsEMHom {obj a} {obj b} {φ a} {φ b} EMap 
 open Eilenberg-Moore-Hom
 
-EMHom : {x y : Obj A} {φ : Hom A (FObj T x) x } {φ' : Hom A (FObj T y) y } {α : Hom A x y }
-          (a : EMObj {x} {φ} ) (b : EMObj {y} {φ'} ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
-EMHom {x} {y} {φ} {φ'} {α} = \a b -> Eilenberg-Moore-Hom {x} {y} {φ} {φ'} {α} a b
+EMHom : (a : EMObj ) (b : EMObj ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
+EMHom = \a b -> Eilenberg-Moore-Hom a b
 
-Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj {x} {φ})
+Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj )
                -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
 Lemma-EM1 {x} {φ} a = let open ≈-Reasoning (A) in
    begin
@@ -83,66 +76,49 @@
        (id1 A x)  o φ
    ∎
 
-EM-id : { a : EMObj } -> EMHom {obj a} {obj a} {phi a} {phi a} {id1 A (obj a)} a a 
-EM-id {a} = record { 
+EM-id : { a : EMObj } -> EMHom a a
+EM-id {a} = record { EMap = id1 A (obj a);
      isEMHom = record { homomorphism = Lemma-EM1 {obj a} {phi a} a } } 
 
 open import Relation.Binary.Core
 
-Lemma-EM2 : {x y z : Obj A}
-            {φ   : Hom A  (FObj T x) x}
-            {φ'  : Hom A  (FObj T y) y}
-            {φ'' : Hom A  (FObj T z) z}
-            {α  : Hom A x y}
-            {α' : Hom A y z}
-            (a : EMObj {x} {φ}   ) 
-            (b : EMObj {y} {φ'}  ) 
-            (c : EMObj {z} {φ''} ) 
-            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c )
-            (f : EMHom {x} {y} {φ} {φ'} {α} a b)
-                 -> A [ A [ φ''  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
-                      ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ ] ]
-Lemma-EM2 {_} {_} {_} {φ} {φ'} {φ''} _ _ _ g f = let 
+Lemma-EM2 : (a : EMObj ) 
+            (b : EMObj ) 
+            (c : EMObj ) 
+            (g : EMHom b c)
+            (f : EMHom a b)
+                 -> A [ A [ φ c  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
+                      ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ a ] ]
+Lemma-EM2 a b c g f = let 
       open ≈-Reasoning (A) in
    begin
-        φ''  o FMap T ((EMap g)  o  (EMap f))
+        φ c  o FMap T ((EMap g)  o  (EMap f))
    ≈⟨ cdr (distr T) ⟩
-        φ''  o ( FMap T (EMap g)  o  FMap T (EMap f) )
+        φ c o ( FMap T (EMap g)  o  FMap T (EMap f) )
    ≈⟨ assoc ⟩
-        ( φ''  o FMap T (EMap g))  o  FMap T (EMap f) 
+        ( φ c o FMap T (EMap g))  o  FMap T (EMap f) 
    ≈⟨ car (IsEMHom.homomorphism (isEMHom g)) ⟩
-        ( EMap g o φ') o  FMap T (EMap f) 
+        ( EMap g o φ b) o  FMap T (EMap f) 
    ≈⟨ sym assoc ⟩
-        EMap g  o (φ' o  FMap T (EMap f) )
+        EMap g  o (φ b o  FMap T (EMap f) )
    ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩
-        EMap g  o (EMap f  o  φ)
+        EMap g  o (EMap f  o  φ a)
    ≈⟨ assoc ⟩
-        ( (EMap g)  o  (EMap f) )  o φ
+        ( (EMap g)  o  (EMap f) )  o φ a
    ∎
 
-_*_ : {x y z : Obj A}
-            {φ   : Hom A  (FObj T x) x}
-            {φ'  : Hom A  (FObj T y) y}
-            {φ'' : Hom A  (FObj T z) z}
-            {α  : Hom A x y}
-            {α' : Hom A y z}
-            {a : EMObj {x} {φ}   } 
-            {b : EMObj {y} {φ'}  } 
-            {c : EMObj {z} {φ''} } 
-            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c ) 
-            (f : EMHom {x} {y} {φ} {φ'} {α} a b) ->
-                (EMHom {x} {z} {φ} {φ''} {A [ α' o  α ] } a c)
-_*_ {x} {y} {z} {φ} {φ'} {φ''} {α} {α'} {a} {b} {c} g f = record { isEMHom = record { homomorphism = 
-     Lemma-EM2 {x} {y} {z} {φ} {φ'} {φ''} {α} {α'} a b c g f } }
+_*_ : {a : EMObj } {b : EMObj } {c : EMObj }
+            (g : EMHom b c ) (f : EMHom a b) -> (EMHom a c)
+_*_ {a} {b} {c} g f = record { EMap = A [ EMap g  o EMap f ] ; isEMHom = record { homomorphism = 
+     Lemma-EM2 a b c g f } }
 
 _∙_ :  {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
 _∙_ {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
 
-_≗_ :  {x y : Obj A} {φ   : Hom A  (FObj T x) x} {φ'  : Hom A  (FObj T y) y} {α α' : Hom A x y} 
-            {a : EMObj {x} {φ} } {b : EMObj {y} {φ'}}
-            (f : EMHom {x} {y} {φ} {φ'} {α}  a b )
-            (g : EMHom {x} {y} {φ} {φ'} {α'} a b ) -> Set ℓ 
-_≗_ {_} {_} {_} {_} {α} {α'} f g = A [ α ≈ α' ]
+_≗_ : {a : EMObj } {b : EMObj }
+            (f : EMHom a b )
+            (g : EMHom a b ) -> Set ℓ 
+_≗_ f g = A [ EMap f ≈ EMap g ]
 
 
 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
@@ -154,9 +130,8 @@
                     }
      where
          open ≈-Reasoning (A) 
-         isEquivalence : {x y : Obj A} {φ   : Hom A  (FObj T x) x} {φ'  : Hom A  (FObj T y) y} {α α' : Hom A x y} 
-            {a : EMObj {x} {φ} } {b : EMObj {y} {φ'}} ->
-               IsEquivalence {_} {_} {EMHom {x} {y} {φ} {φ'} {α}  a b } _≗_
+         isEquivalence : {a : EMObj } {b : EMObj } ->
+               IsEquivalence {_} {_} {EMHom a b } _≗_
          isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl-hom
              ; sym   = sym