# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374905240 -32400
# Node ID c3846bf837176fc4e048d627875fdc364b17984d
# Parent  bb95e780c68f34c6edb151de46bc2676b9f991fd
Comparison Functor

diff -r bb95e780c68f -r c3846bf83717 nat.agda
--- 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
+                     ?
+                  ≈⟨ ?  ⟩
+                     ?
+                  ∎