Mercurial > hg > Members > kono > Proof > category

changeset 118:324950507362

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε^T and μ^t
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2013 10:30:54 +0900
parents d91e89766a76
children 32ef4cdb18a2
files em-category.agda
diffstat 1 files changed, 46 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Thu Aug 01 09:46:56 2013 +0900
+++ b/em-category.agda	Thu Aug 01 10:30:54 2013 +0900
@@ -251,6 +251,52 @@
        isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
        isNTrans1 = record { naturality = naturality1 }
 
+Lemma-EM9 : (a : EMObj) -> A [ A [ (φ a)  o FMap T (φ a) ]  ≈ A [ (φ a)  o (φ (FObj ( F^T ○ U^T ) a)) ] ]
+Lemma-EM9 a = let open ≈-Reasoning (A) in
+          sym ( begin
+              (φ a)  o (φ (FObj ( F^T ○ U^T ) a))
+          ≈⟨⟩
+              (φ a)  o (TMap μ (obj a))
+          ≈⟨ IsAlgebra.eval (isAlgebra a) ⟩
+              (φ a)  o FMap T (φ a)
+          ∎ )
+
+emap-ε : (a : EMObj ) -> EMHom (FObj ( F^T ○ U^T ) a)  a
+emap-ε a = record { EMap = φ a ; homomorphism = Lemma-EM9 a }
+
+ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory  ( F^T ○ U^T ) identityFunctor
+ε^T = record { TMap = \a -> emap-ε a; isNTrans = isNTrans1 } where
+       naturality1 : {a b : EMObj } {f : EMHom a b}
+            →  (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙(  FMap (F^T ○ U^T) f ) )
+       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+          sym ( begin 
+             EMap (( emap-ε b ) ∙ (  FMap (F^T ○ U^T) f ))
+          ≈⟨⟩
+             φ b  o   FMap T (EMap f)
+          ≈⟨ homomorphism f ⟩
+             EMap f  o φ a
+          ≈⟨⟩
+             EMap (f ∙ ( emap-ε a ))
+          ∎  )
+       isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
+       isNTrans1 = record { naturality = naturality1 }
+
+                                                                                 
+--
+-- μ = U^T ε U^F
+--
+
+emap-μ :  (a : Obj A) -> Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
+emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a ))
+
+nat-μ : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
+nat-μ = record { TMap = emap-μ ; isNTrans = isNTrans1 } where
+        naturality1 : {a b : Obj A} {f : Hom A a b}
+             →  A [ A [ (FMap (U^T ○ F^T) f) o  ( emap-μ a) ]  ≈ A [ ( emap-μ b ) o  FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f)  ] ]
+        naturality1 = {!!}
+        isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
+        isNTrans1 = record { naturality = naturality1 }
+
 
 --open MResolution