Mercurial > hg > Members > kono > Proof > category

changeset 83:c3846bf83717

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Comparison Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Jul 2013 15:07:20 +0900
parents bb95e780c68f
children ee25f96ee8cc
files nat.agda
diffstat 1 files changed, 39 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sat Jul 27 14:34:21 2013 +0900
+++ b/nat.agda	Sat Jul 27 15:07:20 2013 +0900
@@ -547,6 +547,45 @@
                ∎
 
 
+module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁ c₂ ℓ ) 
+      { U_K : Functor B A } { F_K : Functor A B }
+      { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
+      { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 
+      ( Adj : Adjunction A B U_K F_K η_K ε_K )
+  where
 
+        kfmap : ?
+        kfmap = ?
 
+        K_T : Functor KleisliCategory B 
+        K_T = record {
+                  FObj = FObj F_K
+                ; FMap = kfmap
+                ; isFunctor = record
+                {      ≈-cong   = ≈-cong
+                     ; identity = identity
+                     ; distr    = distr1
+                }
+             } where
+                identity : {a : Obj B} →  B [ kfmap (K-id {a}) ≈ id1 B (FObj T a) ]
+                identity {a} = let open ≈-Reasoning (B) in
+                  begin
+                      ?
+                  ≈⟨ ? ⟩
+                     ?
+                  ∎
+                ≈-cong : {a b : Obj B} {f g : KHom a b} → B [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
+                ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
+                  begin
+                     ?
+                  ≈⟨ ?  ⟩
+                     ?
+                  ∎
+                distr1 :  {a b c : Obj B} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
+                distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
+                  begin
+                     ?
+                  ≈⟨ ?  ⟩
+                     ?
+                  ∎