# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375263285 -32400
# Node ID 4dec85377dbc73833e5912ecd5cd63e97ad0cf8a
# Parent  b881dbc47684ac903634186d1ce99e7158ef11af
yellow...

diff -r b881dbc47684 -r 4dec85377dbc em-category.agda
--- a/em-category.agda	Wed Jul 31 17:34:17 2013 +0900
+++ b/em-category.agda	Wed Jul 31 18:34:45 2013 +0900
@@ -74,8 +74,8 @@
        isEMHom : IsEMHom a b α
 open Eilenberg-Moore-Hom
 
-EMHom = \(a b : EMObj) -> {α : Hom A (emobj a) (emobj b) } -> 
-         Eilenberg-Moore-Hom {emobj a} {emobj b} {emphi a} {emphi b} a b {α}
+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 {α}
 
 Lemma-EM1 : {x : Obj A}
               {φ : Hom A (FObj T x) x}
@@ -101,18 +101,29 @@
 
 open import Relation.Binary.Core
 
-Lemma-EM2 : (a b c : EMObj) 
-              (φ   : Hom A  (FObj T (emobj a)) (emobj a))
-              (φ'  : Hom A  (FObj T (emobj b)) (emobj b))
-              (φ'' : Hom A  (FObj T (emobj c)) (emobj c))
-              (g : EMHom b c)
-              (f : EMHom a b) -> A [ A [ φ''  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
+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}
+            (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) ] ) ]  
                       ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ ] ]
-Lemma-EM2 (emObj AisAlgebra ) _ (emObj CisAlgebra ) φ φ' φ'' g f = let 
+Lemma-EM2 {_} {_} {_} {φ} {φ'} {φ''} (emObj _) (emObj _) (emObj _) g f = let 
       open ≈-Reasoning (A) in
    begin
-        φ''  o FMap T (A [ (EMap g)  o  (EMap f) ] )
-   ≈⟨ {!!} ⟩
+        φ''  o FMap T ((EMap g)  o  (EMap f))
+   ≈⟨ cdr (distr T) ⟩
+        φ''  o ( FMap T (EMap g)  o  FMap T (EMap f) )
+   ≈⟨ assoc ⟩
+        ( φ''  o FMap T (EMap g))  o  FMap T (EMap f) 
+   ≈⟨ car (IsEMHom.homomorphism (isEMHom g)) ⟩
+        ( EMap g o φ') o  FMap T (EMap f) 
+   ≈⟨ sym assoc ⟩
+        EMap g  o (φ' o  FMap T (EMap f) )
+   ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩
         ( (EMap g)  o  (EMap f) )  o φ
    ∎
 _≗_ : { a : EMObj } { b : EMObj } (f g  : EMHom a b ) -> Set ℓ 
@@ -121,7 +132,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 ( emphi a) (emphi b ) (emphi c) g f } }
+            record { homomorphism = Lemma-EM2 a b c g f } }
 
 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence