Mercurial > hg > Members > kono > Proof > category

changeset 92:ef8f14b862b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
K_T identity
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jul 2013 20:18:32 +0900
parents 3093e70ec20d
children 44b61ce90dd9
files nat.agda
diffstat 1 files changed, 18 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sun Jul 28 19:49:00 2013 +0900
+++ b/nat.agda	Sun Jul 28 20:18:32 2013 +0900
@@ -583,31 +583,36 @@
         kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
         kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (RMap f) ]
 
+        open Adjunction
         K_T : Functor KleisliCategory B 
         K_T = record {
                   FObj = FObj F_K
                 ; FMap = kfmap
                 ; isFunctor = record
-                {      ≈-cong   = {!!} -- ≈-cong
-                     ; identity = {!!} -- identity
+                {      ≈-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
+             } where
+                 identity : {a : Obj A} →  B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
+                 identity {a} = let open ≈-Reasoning (B) in
+                   begin
+                       kfmap (K-id {a})
+                   ≈⟨⟩
+                       TMap ε_K (FObj F_K a) o FMap F_K (RMap (K-id {a}))
+                   ≈⟨⟩
+                      TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
+                   ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
+                      id1 B (FObj F_K a)
+                   ∎
+                 ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ 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 : Obj A} {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
 --                      ?