Mercurial > hg > Members > kono > Proof > category

changeset 93:44b61ce90dd9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
distr continue..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jul 2013 21:24:17 +0900
parents ef8f14b862b5
children 4fa718e4fd77
files nat.agda
diffstat 1 files changed, 32 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sun Jul 28 20:18:32 2013 +0900
+++ b/nat.agda	Sun Jul 28 21:24:17 2013 +0900
@@ -580,6 +580,16 @@
         RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) 
         RKMap {_} {b} f = KtoT f (( ≃-sym (T=UF RK)) (id1 A b))
 
+        RMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ RMap f ≈ RMap g ]
+        RMap-cong {a} {b} {f} {g} eq = helper a b f g eq (( ≃-sym (UF=T RK))( id1 A b  )) 
+          where 
+                open ≈-Reasoning (A)
+                helper : (a b : Obj A) (f g : KHom a b) -> A [ KMap f ≈ KMap g ] ->
+                         {conv : Hom A  (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] conv ~ conv) -> A [ RMap f ≈ RMap g ]
+                helper a b f g eq (Category.Cat.refl {conv} eq2) = 
+                    (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq 
+                        (refl-hom {FObj T b} {FObj ( U_K ○ F_K ) b} {conv} )
+
         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) ]
 
@@ -591,7 +601,7 @@
                 ; isFunctor = record
                 {      ≈-cong   = ≈-cong
                      ; identity = identity
-                     ; distr    = {!!} -- distr1
+                     ; distr    = distr1
                 }
              } where
                  identity : {a : Obj A} →  B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
@@ -606,17 +616,25 @@
                       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 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
---                      ?
---                   ≈⟨ ?  ⟩
---                      ?
---                   ∎
+                 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
+                   begin
+                       kfmap f
+                   ≈⟨⟩
+                       TMap ε_K (FObj F_K b) o FMap F_K (RMap f)
+                   ≈⟨ cdr ( fcong F_K (RMap-cong f≈g))  ⟩
+                       TMap ε_K (FObj F_K b) o FMap F_K (RMap g)
+                   ≈⟨⟩
+                       kfmap g
+                   ∎
+                 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
+                      kfmap (g * f)
+                   ≈⟨⟩
+                      TMap ε_K (FObj F_K c) o FMap F_K (RMap (g * f))
+                   ≈⟨⟩
+                      TMap ε_K (FObj F_K c) o FMap F_K (RMap (A [ (TMap μ c) o A [ (FMap ( U_K ○ F_K ) (RMap g)) o (RMap f) ] ] ))
+                   ≈⟨ {!!}  ⟩
+                      kfmap g o kfmap f
+                   ∎