Mercurial > hg > Members > kono > Proof > category

changeset 116:0e37b2cf3c73

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
F^T and U^T constructed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2013 09:24:53 +0900
parents 17e69b05bc5e
children d91e89766a76
files em-category.agda
diffstat 1 files changed, 41 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Thu Aug 01 09:04:45 2013 +0900
+++ b/em-category.agda	Thu Aug 01 09:24:53 2013 +0900
@@ -164,25 +164,45 @@
         }
      } where open ≈-Reasoning (A) 
 
-Lemma-EM4 : (a : Obj A ) (phi : Hom A (FObj T a) a) -> A [ A [ phi  o TMap η a ] ≈ id1 A a ]
-Lemma-EM4 = ?
+open Monad
+Lemma-EM4 : (x : Obj A ) -> A [ A [ TMap μ x  o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
+Lemma-EM4 x = let  open ≈-Reasoning (A) in
+    begin
+       TMap μ x  o TMap η (FObj T x) 
+    ≈⟨ IsMonad.unity1 (isMonad M) ⟩
+       id1 A (FObj T x)
+    ∎
 
-Lemma-EM5 : (a : Obj A ) (phi : Hom A (FObj T a) a) -> A [ A [ phi  o TMap μ a ] ≈ A [ phi o FMap T phi ] ]
-Lemma-EM5 = ?
+Lemma-EM5 : (x : Obj A ) -> A [ A [ ( TMap μ x)  o TMap μ (FObj T x) ] ≈ A [ ( TMap μ x) o FMap T ( TMap μ x) ] ]
+Lemma-EM5 x =  let  open ≈-Reasoning (A) in
+    begin
+       ( TMap μ x)  o TMap μ (FObj T x) 
+    ≈⟨ IsMonad.assoc (isMonad M) ⟩
+       ( TMap μ x) o FMap T ( TMap μ x)
+    ∎
 
 ftobj : Obj A -> EMObj
 ftobj = \x -> record { a = FObj T x ; phi = TMap μ x; 
  isAlgebra = record {
-      identity = Lemma-EM4 (FObj T x) ( TMap μ x);
-      eval     = Lemma-EM5 (FObj T x) ( TMap μ x)
+      identity = Lemma-EM4 x;
+      eval     = Lemma-EM5 x
  } }
 
-Lemma-EM6 :  (a b : EMObj ) -> (f : Hom A (obj a) (obj b))  -> 
-      A [ A [ (φ b)  o FMap T f ]  ≈ A [ f  o (φ a) ] ]
-Lemma-EM6 = ?
+Lemma-EM6 :  (a b : Obj A ) -> (f : Hom A a b ) ->
+      A [ A [ (φ (ftobj b))  o FMap T (FMap T f) ]  ≈ A [ FMap T f  o (φ (ftobj a)) ] ]
+Lemma-EM6 a b f =  let  open ≈-Reasoning (A) in
+    begin
+       (φ (ftobj b))  o FMap T (FMap T f)
+    ≈⟨⟩
+       TMap μ b  o FMap T (FMap T f)
+    ≈⟨ sym (nat μ) ⟩
+       FMap T f  o TMap μ a
+    ≈⟨⟩
+       FMap T f  o (φ (ftobj a))
+    ∎
 
 ftmap : {a b : Obj A} -> (Hom A a b) -> EMHom (ftobj a) (ftobj b)
-ftmap {a} {b} f = record { EMap = FMap T f; homomorphism =  Lemma-EM6 (ftobj a) (ftobj b) (FMap T f) }
+ftmap {a} {b} f = record { EMap = FMap T f; homomorphism =  Lemma-EM6 a b f }
 
 F^T : Functor A Eilenberg-MooreCategory
 F^T = record {
@@ -191,22 +211,22 @@
         ; isFunctor = record {
                ≈-cong   = ≈-cong   
              ; identity = identity 
-             ; distr    = distr 
+             ; distr    = distr1 
         }
      } where 
         ≈-cong   : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → (ftmap f) ≗ (ftmap g)
-        ≈-cong   = ?
+        ≈-cong   = let  open ≈-Reasoning (A) in ( fcong T )
         identity :  {a : Obj A} →  ftmap (id1 A a) ≗ EM-id {ftobj a}
-        identity = ?
-        distr    :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
-        distr    = ?
+        identity = IsFunctor.identity ( isFunctor T )
+        distr1    :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
+        distr1    =  let  open ≈-Reasoning (A) in ( distr T )
 
 --open MResolution
---
---Resolution_T : MResolution A Eilenberg-MooreCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T 
---Resolution_T = record {
---      T=UF   = Lemma11;
---      μ=UεF  = Lemma12 
---  }
+
+--Resolution^T : MResolution A Eilenberg-MooreCategory T^U_T F^T {η^t} {ε^T} {μ^T} Adj_T 
+--Resolution^T = record {
+--        T=UF   = Lemma-EM7;
+--        μ=UεF  = Lemma-EM8 
+--}
 
 -- -- end