# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375293028 -32400
# Node ID 2032c438b6a6239643a5a6a77f95cc0c32893984
# Parent  239fa20251ece12dd6a6200e5e91464d88ac810a
EM Category constructed

diff -r 239fa20251ec -r 2032c438b6a6 em-category.agda
--- a/em-category.agda	Thu Aug 01 01:45:17 2013 +0900
+++ b/em-category.agda	Thu Aug 01 02:50:28 2013 +0900
@@ -31,33 +31,27 @@
 --
 open Functor
 open NTrans
-record IsEMObj (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+
+record IsAlgebra {a : Obj A} { phi : Hom A (FObj T a) a } : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
    field
-       identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
-       eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
-open IsEMObj
+       identity : A [ A [ phi  o TMap η a ] ≈ id1 A a ]
+       eval     : A [ A [ phi  o TMap μ a ] ≈ A [ phi o FMap T phi ] ]
 
 record EMObj : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
    field
-       a : Obj A
-       phi : Hom A (FObj T a) a
-       isEMObj : IsEMObj a phi 
+       a         : Obj A
+       phi       : Hom A (FObj T a) a
+       isAlgebra : IsAlgebra {a} {phi}
    obj : Obj A
    obj = 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) : Set ℓ where
-   field
-       homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
-open IsEMHom
-
 record Eilenberg-Moore-Hom (a : EMObj ) (b : EMObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
    field
        EMap    : Hom A (obj a) (obj b)
-       isEMHom : IsEMHom {obj a} {obj b} {φ a} {φ b} EMap 
+       homomorphism : A [ A [ (φ b)  o FMap T EMap ]  ≈ A [ EMap  o (φ a) ] ]
 open Eilenberg-Moore-Hom
 
 EMHom : (a : EMObj ) (b : EMObj ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
@@ -78,7 +72,7 @@
 
 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 } } 
+     homomorphism = Lemma-EM1 {obj a} {phi a} a } 
 
 open import Relation.Binary.Core
 
@@ -97,36 +91,28 @@
         φ c o ( FMap T (EMap g)  o  FMap T (EMap f) )
    ≈⟨ assoc ⟩
         ( φ c o FMap T (EMap g))  o  FMap T (EMap f) 
-   ≈⟨ car (IsEMHom.homomorphism (isEMHom g)) ⟩
+   ≈⟨ car (homomorphism (g)) ⟩
         ( EMap g o φ b) o  FMap T (EMap f) 
    ≈⟨ sym assoc ⟩
         EMap g  o (φ b o  FMap T (EMap f) )
-   ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩
+   ≈⟨ cdr (homomorphism (f)) ⟩
         EMap g  o (EMap f  o  φ a)
    ≈⟨ assoc ⟩
         ( (EMap g)  o  (EMap f) )  o φ a
    ∎
 
-_*_ : {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 { 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 } }
-
-_≗_ : {a : EMObj } {b : EMObj }
-            (f : EMHom a b )
-            (g : EMHom a b ) -> Set ℓ 
+_≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) -> Set ℓ 
 _≗_ f g = A [ EMap f ≈ EMap g ]
 
-
 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
-                    ; identityL =   EMidL
-                    ; identityR =   EMidR
-                    ; o-resp-≈ =    EMo-resp
-                    ; associative = EMassoc
+                    ; identityL =   IsCategory.identityL (Category.isCategory A)
+                    ; identityR =   IsCategory.identityR (Category.isCategory A)
+                    ; o-resp-≈ =    IsCategory.o-resp-≈ (Category.isCategory A)
+                    ; associative = IsCategory.associative (Category.isCategory A)
                     }
      where
          open ≈-Reasoning (A) 
@@ -137,16 +123,19 @@
              ; sym   = sym
              ; trans = trans-hom
              } 
-         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 {C})  ≗ f
-         EMidR {_} {_} {f} =  idR
-         EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
+--
+-- cannot use as identityL = EMidL
+--
+EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id  ∙ f) ≗ f
+EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D} 
+EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id)  ≗ f
+EMidR {C} {_} {_} = let open ≈-Reasoning (A) in  idR {obj C}
+EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
                           f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
-         EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
-         EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
+EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
+EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
                           (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
-         EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
+EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
 
 Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
 Eilenberg-MooreCategory =