# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375268829 -32400
# Node ID da14b7f03ff8e316be4dddc2fbe20070e9e77602
# Parent  4dec85377dbc73833e5912ecd5cd63e97ad0cf8a
no yellow. ready to define category

diff -r 4dec85377dbc -r da14b7f03ff8 em-category.agda
--- a/em-category.agda	Wed Jul 31 18:34:45 2013 +0900
+++ b/em-category.agda	Wed Jul 31 20:07:09 2013 +0900
@@ -69,22 +69,19 @@
               (a : EMObj {x} {φ}) 
               (b : EMObj {y} {φ'}) 
               {α : Hom A x y} : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+   EMap    : Hom A x y
+   EMap    = α
    field
-       EMap    : Hom A x y
        isEMHom : IsEMHom a b α
 open Eilenberg-Moore-Hom
 
-EMHom = \(a : EMObj) (b : EMObj) -> {α : Hom A (emobj a) (emobj b) } -> 
-         Eilenberg-Moore-Hom {emobj a} {emobj b} {emphi {emobj a} a } {emphi b} a b {α}
+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 {α}
 
-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 {x} {φ})
                -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
-Lemma-EM1 (emObj isAlgebra ) = let 
-         x = obj isAlgebra
-         φ = phi isAlgebra
-         open ≈-Reasoning (A) in
+Lemma-EM1 {x} {φ} (emObj isAlgebra ) = let open ≈-Reasoning (A) in
    begin
        φ o FMap T (id1 A x)
    ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
@@ -95,9 +92,9 @@
        (id1 A x)  o φ
    ∎
 
-EM-id : {a : EMObj } -> EMHom a a 
-EM-id  {a = a} = record { EMap = id1 A (emobj a) ; 
-     isEMHom = record { homomorphism = Lemma-EM1 a } }
+EM-id : {x : Obj A} {φ : Hom A (FObj T x) x} {a : EMObj {x} {φ} } -> EMHom a a 
+EM-id {x} {φ} {a = a} = record { 
+     isEMHom = record { homomorphism = Lemma-EM1 {x} {φ} a } } 
 
 open import Relation.Binary.Core
 
@@ -105,13 +102,16 @@
             {φ   : 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 b c)
-            (f : EMHom a b) -> A [ A [ φ''  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
+            (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 {_} {_} {_} {φ} {φ'} {φ''} (emObj _) (emObj _) (emObj _) g f = let 
+Lemma-EM2 {_} {_} {_} {φ} {φ'} {φ''} _ _ _ g f = let 
       open ≈-Reasoning (A) in
    begin
         φ''  o FMap T ((EMap g)  o  (EMap f))
@@ -124,6 +124,8 @@
    ≈⟨ sym assoc ⟩
         EMap g  o (φ' o  FMap T (EMap f) )
    ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩
+        EMap g  o (EMap f  o  φ)
+   ≈⟨ assoc ⟩
         ( (EMap g)  o  (EMap f) )  o φ
    ∎
 _≗_ : { a : EMObj } { b : EMObj } (f g  : EMHom a b ) -> Set ℓ 
@@ -131,8 +133,7 @@
 
 _∙_ : { a b c : EMObj } → 
                       ( EMHom b c) → (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} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
 
 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence