Mercurial > hg > Members > kono > Proof > category

changeset 123:44c58c27d12d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
problems written Comparison Functor on EM
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2013 08:36:44 +0900
parents f8fbd5ecec97
children aaeb92b58647
files comparison-em.agda
diffstat 1 files changed, 18 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/comparison-em.agda	Fri Aug 02 08:21:32 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 08:36:44 2013 +0900
@@ -33,10 +33,13 @@
 
 T^K = U^K ○ F^K
 
-M : Monad A (U^K ○ F^K ) η^K μ^K 
+μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) 
+μ^K'  = UεF A B U^K F^K ε^K 
+
+M : Monad A (U^K ○ F^K ) η^K μ^K' 
 M =  Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K
 
-open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } 
+open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K' } { M } 
 
 open Functor
 open NTrans
@@ -46,7 +49,7 @@
 
 emkobj : Obj B -> EMObj
 emkobj b = record { 
-     a = FObj U^K b ; phi = A [ FMap U^K o TMap ε^K b ] ; isAlgebra = record { identity = identity1; eval = eval1 }
+     a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1; eval = eval1 }
   } where
       identity1 : ?
       identity1 = ?
@@ -69,25 +72,25 @@
              ; distr    = distr1
         }
      }  where
-         identity : {a : Obj A} →  B [ emkmap (EM-id {a}) ≈ id1 B (FObj F^K a) ]
-         identity {a} = let open ≈-Reasoning (B) in
+         identity : {a : Obj B} →   emkmap (id1 B a) ≗ EM-id {emkobj a}
+         identity {a} = let open ≈-Reasoning (A) in
            begin
-               emkmap (EM-id {a})
+              EMap (emkmap (id1 B a))
            ≈⟨ ? ⟩
-              id1 B (FObj F^K a)
+              EMap (EM-id {emkobj a})
            ∎
-         ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → B [ emkmap f ≈ emkmap g ]
-         ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
+         ≈-cong : {a b : Obj B} -> {f g : Hom B a b} → B [ f ≈ g ] →  emkmap f ≗ emkmap g 
+         ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
            begin
-               emkmap f
+               EMap (emkmap f)
            ≈⟨ ? ⟩
-               emkmap g
+               EMap (emkmap g)
            ∎
-         distr1 :  {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g ∙ f) ≈ (B [ emkmap g o emkmap f ] )]
-         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
+         distr1 :  {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → ( (emkmap (B [ g o f ])) ≗  (emkmap g ∙ emkmap f)  )
+         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
            begin
-              emkmap (g ∙ f)
+              EMap (emkmap (B [ g o f ] ))
            ≈⟨ ? ⟩
-              emkmap g o emkmap f
+              EMap (emkmap g ∙ emkmap f)
            ∎