Mercurial > hg > Members > kono > Proof > category

changeset 128:276f33602700

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Comparison Functor all done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2013 17:01:14 +0900
parents 3e05417b0876
children fdf89038556a
files category.ind comparison-em.agda comparison-functor.agda
diffstat 3 files changed, 56 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/category.ind	Fri Aug 02 10:06:15 2013 +0900
+++ b/category.ind	Fri Aug 02 17:01:14 2013 +0900
@@ -1385,7 +1385,7 @@
 \end{tikzcd}
 
 
---Vertial Compositon  $ε・ε$
+--Vertcial Compositon  $ε・ε$
 
 $  ε・ε : FUFU -> 1B$
 
--- 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)
+           ∎
+
+
+
--- a/comparison-functor.agda	Fri Aug 02 10:06:15 2013 +0900
+++ b/comparison-functor.agda	Fri Aug 02 17:01:14 2013 +0900
@@ -180,7 +180,8 @@
                  id1 B (FObj F_K b)
            ∎
 
-Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) -> B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] })  ≈ FMap F_K g ]
+Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) -> 
+     B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] })  ≈ FMap F_K g ]
 Lemma-K4 b c g = let open ≈-Reasoning (B) in
            begin
                 FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] }) 
@@ -196,3 +197,20 @@
                 FMap F_K g 
            ∎
 
+-- Lemma-K5 : (a : Obj A) -> FObj U_K ( FObj K_T a ) = U_T a
+
+Lemma-K6 : (b c : Obj A) (g : KHom b c) -> A [ FMap U_K ( FMap K_T g )  ≈ FMap U_T g ]
+Lemma-K6 b c g =  let open ≈-Reasoning (A) in
+           begin
+                 FMap U_K ( FMap K_T g )
+           ≈⟨⟩
+                 FMap U_K ( B [ TMap ε_K ( FObj F_K c )  o FMap F_K (KMap g) ] )
+           ≈⟨ distr U_K ⟩
+                 FMap U_K ( TMap ε_K ( FObj F_K c ))  o FMap U_K ( FMap F_K (KMap g) )
+           ≈⟨⟩
+                 TMap μ_K c o FMap U_K ( FMap F_K (KMap g) )
+           ≈⟨⟩
+                 FMap U_T g
+           ∎
+
+