Mercurial > hg > Members > kono > Proof > category

changeset 105:b881dbc47684

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 17:34:17 +0900
parents 53a79dfdcd04
children 4dec85377dbc
files em-category.agda
diffstat 1 files changed, 30 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Wed Jul 31 16:33:59 2013 +0900
+++ b/em-category.agda	Wed Jul 31 17:34:17 2013 +0900
@@ -32,27 +32,27 @@
 open Functor
 open NTrans
 record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
-   obj : Obj A
-   obj = a
-   phi : Hom A (FObj T a) a
-   phi = φ
    field
        identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
        eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
 open IsEMAlgebra
 
 record EMAlgebra (a : Obj A)  (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
-  field
+   obj : Obj A
+   obj = a
+   phi : Hom A (FObj T a) a
+   phi = φ
+   field
      isEMAlbgebra : IsEMAlgebra a φ 
 open EMAlgebra
      
-data EMObj {a : Obj A}  {φ  : Hom A (FObj T a) a }  : Set ( c₁ ⊔ c₂  ⊔ ℓ) where
-            emObj : (IsEMAlgebra a φ) -> EMObj {a} {φ}
+data EMObj {a : Obj A}  {φ : Hom A (FObj T a) a }  : Set ( c₁ ⊔ c₂  ⊔ ℓ) where
+            emObj  : (EMAlgebra a φ) -> EMObj {a} {φ}
 
-emobj : EMObj -> Obj A
+emobj : {a : Obj A} -> {φ : Hom A (FObj T a) a } -> EMObj {a} {φ} -> Obj A
 emobj (emObj isAlgebra) = obj isAlgebra
 
-emphi : EMObj -> ? -- {a : Obj A} -> ? -- Hom A (FObj T a ) a
+emphi : {a : Obj A} -> {φ : Hom A (FObj T a) a } -> EMObj {a} {φ} -> Hom A (FObj T a) a
 emphi (emObj isAlgebra) = phi isAlgebra 
 
 record IsEMHom {x y : Obj A} {φ  : Hom A (FObj T x) x } {φ'  : Hom A (FObj T y) y }
@@ -64,14 +64,18 @@
 open IsEMHom
 
 record Eilenberg-Moore-Hom {x y : Obj A }
-              (a : EMObj {x}) 
-              (b : EMObj {y}) 
+              {φ  : Hom A (FObj T x) x } 
+              {φ' : Hom A (FObj T y) y } 
+              (a : EMObj {x} {φ}) 
+              (b : EMObj {y} {φ'}) 
               {α : Hom A x y} : Set (c₁ ⊔ c₂ ⊔ ℓ) where
    field
-       EMap :  Hom A x y
+       EMap    : Hom A x y
        isEMHom : IsEMHom a b α
 open Eilenberg-Moore-Hom
-EMHom = \(a b : EMObj) -> Eilenberg-Moore-Hom {emobj a} {emobj b} a b 
+
+EMHom = \(a b : EMObj) -> {α : Hom A (emobj a) (emobj b) } -> 
+         Eilenberg-Moore-Hom {emobj a} {emobj b} {emphi a} {emphi b} a b {α}
 
 Lemma-EM1 : {x : Obj A}
               {φ : Hom A (FObj T x) x}
@@ -98,16 +102,17 @@
 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 [ (emphi c)  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
-                      ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o (emphi c) ] ]
-Lemma-EM2 _ _ (emObj isAlgebra ) g f = let 
-      x = obj isAlgebra
-      φ = phi isAlgebra
+              (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 
       open ≈-Reasoning (A) in
    begin
-        φ  o FMap T (A [ (EMap g)  o  (EMap f) ] )
-   ≈⟨ ? ⟩
+        φ''  o FMap T (A [ (EMap g)  o  (EMap f) ] )
+   ≈⟨ {!!} ⟩
         ( (EMap g)  o  (EMap f) )  o φ
    ∎
 _≗_ : { a : EMObj } { b : EMObj } (f g  : EMHom a b ) -> Set ℓ 
@@ -116,7 +121,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 } }
+            record { homomorphism = Lemma-EM2 a b c ( emphi a) (emphi b ) (emphi c) g f } }
 
 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
@@ -135,15 +140,15 @@
              ; trans = trans-hom
              } 
          KidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
-         KidL {_} {_} {f} =  ? -- Lemma7 (EMap f) 
+         KidL {_} {_} {f} =  {!!} -- Lemma7 (EMap f) 
          KidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
-         KidR {_} {_} {f} =  ? -- Lemma8 (EMap f) 
+         KidR {_} {_} {f} =  {!!} -- Lemma8 (EMap f) 
          Ko-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
                           f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
-         Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = ? -- Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi
+         Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = {!!} -- Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi
          Kassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
                           (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
-         Kassoc {_} {_} {_} {_} {f} {g} {h} =  ? -- Lemma9 (EMap f) (EMap g) (EMap h) 
+         Kassoc {_} {_} {_} {_} {f} {g} {h} =  {!!} -- Lemma9 (EMap f) (EMap g) (EMap h) 
 
 Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
 Eilenberg-MooreCategory =