Mercurial > hg > Members > kono > Proof > category

changeset 91:3093e70ec20d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
strange but worked.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jul 2013 19:49:00 +0900
parents 2d8da9d745c5
children ef8f14b862b5
files cat-utility.agda nat.agda
diffstat 2 files changed, 7 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sun Jul 28 19:08:26 2013 +0900
+++ b/cat-utility.agda	Sun Jul 28 19:49:00 2013 +0900
@@ -144,6 +144,7 @@
                    -- MMap f = FMap ( UR ○ FR ) f
                    field
                       T=UF  :  T ≃  (UR ○ FR) 
+                      UF=T  :  (UR ○ FR) ≃ T
                       μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
                       -- ηR=η  : {x : Obj A } -> A [ TMap ηR x  ≈  TMap η x ]
                       -- μR=μ  : {x : Obj A } -> A [ TMap μR x  ≈  TMap μ x ]
--- a/nat.agda	Sun Jul 28 19:08:26 2013 +0900
+++ b/nat.agda	Sun Jul 28 19:49:00 2013 +0900
@@ -568,17 +568,17 @@
                    Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf)
 
         RHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
-        TtoK : {a b : Obj A} -> (f : KHom a b) -> {g h : Hom A  (FObj T b) (FObj ( U_K ○ F_K ) b) } ->
-              ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b)  
+        TtoK : {a b : Obj A} -> (KHom a b) ->  {g : Hom A  (FObj T b) (FObj ( U_K ○ F_K) b) } -> 
+              ([ A ] g ~ g) -> Hom A a (FObj ( U_K ○ F_K ) b)  
         TtoK  f (Category.Cat.refl {g} eq) = A [ g o (KMap f) ]
         RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) 
-        RMap  {a} {b} f = TtoK f {!!} -- ((T=UF RK) (id1 A b))
+        RMap  {a} {b} f = TtoK f (( ≃-sym (UF=T RK))(id1 A b))
 
-        KtoT : {a b : Obj A} -> (f : RHom a b) -> {g h : Hom A  (FObj ( U_K ○ F_K ) b) (FObj  T b) } ->
-              ([ A ] g ~ h) -> Hom A a (FObj T b)  
+        KtoT : {a b : Obj A} -> (RHom a b) -> {g : Hom A  (FObj ( U_K ○ F_K ) b) (FObj  T b) } ->
+              ([ A ] g ~ g) -> Hom A a (FObj T b)  
         KtoT  f (Category.Cat.refl {g} eq) = A [ g o (KMap f) ]
         RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) 
-        RKMap {a} {b} f = KtoT f (( ≃-sym (T=UF RK)) (id1 A b))
+        RKMap {_} {b} f = KtoT f (( ≃-sym (T=UF RK)) (id1 A b))
 
         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) ]