Mercurial > hg > Members > kono > Proof > category

changeset 99:bd542a1caf08

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
uniquness of comparison functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2013 18:27:24 +0900
parents b0ba34a27783
children 59dec035602c
files comparison-functor.agda
diffstat 1 files changed, 60 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/comparison-functor.agda	Mon Jul 29 16:49:11 2013 +0900
+++ b/comparison-functor.agda	Mon Jul 29 18:27:24 2013 +0900
@@ -32,6 +32,8 @@
 
 open import adj-monad
 
+T_K = U_K ○ F_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 
 
@@ -136,3 +138,61 @@
               kfmap g o kfmap f
            ∎
 
+Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) -> B [ FMap K_T ( FMap F_T f)  ≈ FMap F_K f ]
+Lemma-K1 {a} {b} f = let open ≈-Reasoning (B) in
+           begin
+             FMap K_T ( FMap F_T f)  
+           ≈⟨⟩
+             TMap ε_K (FObj F_K b) o FMap F_K (KMap( FMap F_T f))
+           ≈⟨⟩
+             TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ])
+           ≈⟨ cdr ( distr F_K) ⟩
+             TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b)  o FMap F_K f )
+           ≈⟨ assoc  ⟩
+             (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b))  o FMap F_K f 
+           ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩
+             id1 B (FObj F_K b)  o FMap F_K f 
+           ≈⟨ idL  ⟩
+             FMap F_K f 
+           ∎
+
+Lemma-K2 : {a b : Obj A} ( f : KHom a b ) -> A [ FMap U_K ( FMap K_T f)  ≈ FMap U_T f ]
+Lemma-K2 {a} {b} f = let open ≈-Reasoning (A) in
+           begin
+              FMap U_K ( FMap K_T f)
+           ≈⟨⟩
+              FMap U_K ( B [  TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] )
+           ≈⟨ distr U_K ⟩
+              FMap U_K ( TMap ε_K (FObj F_K b)) o FMap U_K (FMap F_K (KMap f) )
+           ≈⟨⟩  
+              TMap μ_K b o FMap T_K (KMap f) 
+           ≈⟨⟩  -- the definition
+              FMap U_T f
+           ∎
+
+Lemma-K3 : (b : Obj A)  -> B [ FMap K_T (record { KMap = (TMap η_K b) }) ≈ id1 B (FObj F_K b) ]
+Lemma-K3 b = let open ≈-Reasoning (B) in
+           begin
+                 FMap K_T  (record { KMap = (TMap η_K b) })
+           ≈⟨⟩  
+                 TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)
+           ≈⟨  IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩  
+                 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 g = let open ≈-Reasoning (B) in
+           begin
+                FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] }) 
+           ≈⟨⟩
+                TMap ε_K (FObj F_K (FObj T_K c)) o FMap F_K (A [ (TMap η_K (FObj T_K c)) o g ])
+           ≈⟨ cdr (distr F_K) ⟩
+                TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)) o FMap F_K g )
+           ≈⟨ assoc ⟩
+                (TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)))) o FMap F_K g 
+           ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩  
+                 id1 B (FObj F_K (FObj T_K c)) o FMap F_K g 
+           ≈⟨ idL ⟩
+                FMap F_K g 
+           ∎
+