--- a/comparison-em.agda	Fri Aug 02 10:06:15 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 17:01:14 2013 +0900
@@ -133,3 +133,39 @@
               EMap (emkmap g ∙ emkmap f)
            ∎
 
+Lemma-EM20 : { a b : Obj B} { f : Hom B a b } -> A [ FMap U^T ( FMap K^T f)  ≈ FMap U^K f ]
+Lemma-EM20 {a} {b} {f}  =  let open ≈-Reasoning (A) in 
+           begin
+               FMap U^T ( FMap K^T f) 
+           ≈⟨⟩
+               FMap U^K f 
+           ∎
+
+-- Lemma-EM21 : { a : Obj B}  -> FObj U^T ( FObj K^T a)  = FObj U^K a 
+
+Lemma-EM22 : { a b : Obj A} { f : Hom A a b } ->  A [ EMap ( FMap K^T ( FMap F^K f) ) ≈ EMap ( FMap F^T f  ) ]
+Lemma-EM22  {a} {b} {f} =  let open ≈-Reasoning (A) in 
+           begin
+                EMap ( FMap K^T ( FMap F^K f) )
+           ≈⟨⟩
+                FMap U^K ( FMap F^K f)
+           ≈⟨⟩
+                EMap ( FMap F^T f  )
+           ∎
+ 
+
+-- Lemma-EM23 : { a b : Obj A}  ->  ( FObj K^T ( FObj F^K f) ) = ( FObj F^T f  ) 
+
+-- Lemma-EM24 :  {a : Obj A } {b : Obj B} -> A [ TMap η^K (FObj U^K b) ≈ TMap η^K a ]
+-- Lemma-EM24 = ?
+
+Lemma-EM26 : {b : Obj B} -> A [ EMap (TMap ε^T ( FObj K^T b)) ≈ FMap U^K ( TMap ε^K b) ]
+Lemma-EM26  {b} =  let open ≈-Reasoning (A) in 
+           begin
+                 EMap (TMap ε^T ( FObj K^T b))
+           ≈⟨⟩
+                 FMap U^K ( TMap ε^K b)
+           ∎
+
+
+