Mercurial > hg > Members > kono > Proof > category

changeset 52:0fc0dbda7b55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nat-ε proved
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jul 2013 16:18:21 +0900
parents adc6bd3c9270
children b4530a807918
files universal-mapping.agda
diffstat 1 files changed, 20 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Tue Jul 23 16:01:25 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 16:18:21 2013 +0900
@@ -18,7 +18,7 @@
    field
        universalMapping :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> 
                      A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
-       uniquness :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (F a') b' } -> 
+       uniquness :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (F a') b' } -> 
                      A [ A [ FMap U g o  η a' ]  ≈ f ] -> B [ f * ≈ g ]
 
 record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
@@ -102,9 +102,9 @@
                 A [ A [ FMap U g o  TMap η a ]  ≈ f ] ->
                 B [  (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] 
          lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
-         uniqness :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (FObj F a') b'} -> 
+         uniqness :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (FObj F a') b'} -> 
                      A [ A [ FMap U g o  TMap η a' ]  ≈ f ] -> B [ solution f  ≈ g ]
-         uniqness a b {f} {g} k = let open ≈-Reasoning (B) in
+         uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
               begin 
                   solution f 
               ≈⟨⟩
@@ -160,7 +160,7 @@
            η a o id a
        ∎
     lemma-id :  {a : Obj A} →  B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ]
-    lemma-id {a} =   ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F a)   lemma-id1
+    lemma-id {a} =   ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) lemma-id1
     lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → 
                 A [ A [ FMap U ((_* um) (A [ η b  o  g ]) ) o  η a ] ≈  A [ η b  o  f ] ]
     lemma-cong2 a b f g eq =  let open ≈-Reasoning (A) in
@@ -172,7 +172,7 @@
           η b  o  f 
        ∎
     lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b  o  f ] ) ≈  (_* um) (A [ η b  o  g ]) ]
-    lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F b)  ( lemma-cong2 a b f g eq )
+    lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) ( lemma-cong2 a b f g eq )
     lemma-cong :  {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ]
     lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq
     lemma-distr2 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → 
@@ -195,7 +195,7 @@
        ∎
     lemma-distr1 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → 
             B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] )]
-    lemma-distr1 a b c f g =  ( IsUniversalMapping.uniquness ( isUniversalMapping um ) a (F c)) (lemma-distr2 a b c f g )
+    lemma-distr1 a b c f g =  ( IsUniversalMapping.uniquness ( isUniversalMapping um )) (lemma-distr2 a b c f g )
     lemma-distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )]
     lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g 
     myIsFunctor : IsFunctor A B F myFMap
@@ -266,6 +266,18 @@
        ≈⟨ sym idR ⟩
           FMap U f o id (FObj U a) 
        ∎
+    lemma-nat2 : (a b : Obj B) (f : Hom B a b ) -> A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ]
+                                                        ≈ A [ FMap U f o id1 A (FObj U a) ] ]
+    lemma-nat2 a b f = let open ≈-Reasoning (A) in
+       begin
+          FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ])  o η (FObj U a) 
+       ≈⟨ car ( IsFunctor.distr ( isFunctor U ) ) ⟩
+          (FMap U f o FMap U ((um *) (id1 A (FObj U a ))))  o η (FObj U a) 
+       ≈⟨ sym assoc  ⟩
+          FMap U f o ( FMap U ((um *) (id1 A (FObj U a )))  o η (FObj U a)  )
+       ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
+          FMap U f o id (FObj U a )
+       ∎
     naturality : {a b : Obj B} {f : Hom B a b }
       →  B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ]
     naturality {a} {b} {f} = let open ≈-Reasoning (B) in
@@ -275,9 +287,9 @@
           ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
        ≈⟨⟩
           ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
-       ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (FObj U a) b ) (lemma-nat1 a b f)) ⟩
+       ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-nat1 a b f))) ⟩
           (_* um) ( A [ FMap U f o id1 A (FObj U a) ] )
-       ≈⟨ {!!} ⟩
+       ≈⟨ (IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-nat2 a b f)) ⟩
           f o  ((_* um) ( id1 A (FObj U a)))
        ≈⟨⟩
           f o  (ε a)