# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375282416 -32400
# Node ID 5f8d6d1aece451f80e5b6a08e29dfcb590d20424
# Parent  c670d0e6b1e29663a9b35d981f6058d02ebe0c38
constructed but some yellow remains

diff -r c670d0e6b1e2 -r 5f8d6d1aece4 em-category.agda
--- a/em-category.agda	Wed Jul 31 21:59:02 2013 +0900
+++ b/em-category.agda	Wed Jul 31 23:53:36 2013 +0900
@@ -47,9 +47,9 @@
 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} {φ'}) 
-              (α : Hom A x y) : Set ℓ where
+              (b : EMObj {y} {φ'}) : Set ℓ where
    field
        homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
 open IsEMHom
@@ -57,18 +57,18 @@
 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} {φ'}) 
-              {α : Hom A x y} : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+              (b : EMObj {y} {φ'}) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
    EMap    : Hom A x y
    EMap    = α
    field
-       isEMHom : IsEMHom a b α
+       isEMHom : IsEMHom {x} {y} {φ} {φ'} α a b 
 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 {x} {y} {φ} {φ'} {α} = \a b -> Eilenberg-Moore-Hom {x} {y} {φ} {φ'} {α} a b
 
 Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj {x} {φ})
                -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
@@ -83,9 +83,9 @@
        (id1 A x)  o φ
    ∎
 
-EM-id : {x : Obj A} {φ : Hom A (FObj T x) x} {a : EMObj {x} {φ} } -> EMHom {x} {x} {φ} {φ} {id1 A x} a a 
-EM-id {x} {φ} {a} = record { 
-     isEMHom = record { homomorphism = Lemma-EM1 {x} {φ} a } } 
+EM-id : { a : EMObj } -> EMHom {obj a} {obj a} {phi a} {phi a} {id1 A (obj a)} a a 
+EM-id {a} = record { 
+     isEMHom = record { homomorphism = Lemma-EM1 {obj a} {phi a} a } } 
 
 open import Relation.Binary.Core
 
@@ -162,9 +162,9 @@
              ; sym   = sym
              ; trans = trans-hom
              } 
-         EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
+         EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id {D} ∙ f) ≗ f
          EMidL {a} {b} {f} =  idL 
-         EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
+         EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id {C})  ≗ f
          EMidR {_} {_} {f} =  idR
          EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
                           f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
@@ -177,9 +177,9 @@
 Eilenberg-MooreCategory =
   record { Obj = EMObj
          ; Hom = EMHom
-         ; _o_ = _∙_
+         ; _o_ = _∙_ 
          ; _≈_ = _≗_
-         ; Id  = EM-id
+         ; Id  =  EM-id 
          ; isCategory = isEilenberg-MooreCategory
           }
 
@@ -201,7 +201,7 @@
 -- --              ; distr    = distr1
 -- --         }
 -- --      } where
--- --         identity : {a : EMObj} →  A [ ufmap (EM-id {a}) ≈ id1 A (FObj T a) ]
+-- --         identity : {a : EMObj} →  A [ ufmap (EM-id a) ≈ id1 A (FObj T a) ]
 -- --         identity {a} = let open ≈-Reasoning (A) in
 -- --           begin
 -- --               TMap μ (a)  o FMap T (TMap η a)