Mercurial > hg > Members > kono > Proof > category

changeset 51:adc6bd3c9270

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jul 2013 16:01:25 +0900
parents b518af3a9b07
children 0fc0dbda7b55
files universal-mapping.agda
diffstat 1 files changed, 37 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Tue Jul 23 10:27:24 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 16:01:25 2013 +0900
@@ -16,9 +16,9 @@
                  ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
-       universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
+       universalMapping :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> 
                      A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
-       unique-universalMapping :   (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₂' ℓ') 
@@ -72,14 +72,14 @@
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
-                    unique-universalMapping = uniqness
+                    uniquness = uniqness
               }
       } where
          solution :  { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) ->  Hom B (FObj F a ) b 
          solution  {_} {b} f = B [ TMap ε b o FMap F f ]
-         universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
+         universalMapping :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> 
                      A [ A [ FMap U ( solution f) o TMap η a' ]  ≈ f ]
-         universalMapping a b {f} = 
+         universalMapping {a} {b} {f} = 
            let open ≈-Reasoning (A) in
               begin 
                   FMap U ( solution  f) o TMap η a 
@@ -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,21 +160,19 @@
            η 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.unique-universalMapping ( isUniversalMapping um ) ) 
-              a (F a)  ((A [ (η a) o (id1 A a)] )) ((id1 B (F a))) lemma-id1
+    lemma-id {a} =   ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F a)   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
        begin
           ( FMap U ((_* um) (A [ η b  o  g ]) )) o  η a 
-       ≈⟨  ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b)  ⟩
+       ≈⟨  ( IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
           η b  o  g 
        ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom)  ) ⟩
           η 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.unique-universalMapping ( isUniversalMapping um ) ) 
-              a (F b) (A [ η b  o  f ])  ((_* um) (A [ η b  o  g ])) ( lemma-cong2 a b f g eq )
+    lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F b)  ( 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) → 
@@ -186,19 +184,18 @@
            (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b  o f ])))) )   o  η a 
        ≈⟨ sym assoc ⟩
            ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b  o f ]))))   o  η a )
-       ≈⟨ cdr ( ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b)) ⟩
+       ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
            ( FMap U ((_* um) (A [ η c o g ])) o ( η b  o f) )
        ≈⟨ assoc ⟩
            ( FMap U ((_* um) (A [ η c o g ])) o  η b)  o f
-       ≈⟨ car (( IsUniversalMapping.universalMapping ( isUniversalMapping um )) b (F c)) ⟩
+       ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
            (  η c o g )  o f
        ≈⟨ sym assoc  ⟩
             η c o ( g o f )
        ∎
     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.unique-universalMapping ( isUniversalMapping um ) a (F c)
-              (A [ η c o A [ g o f ] ]) ((B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] )) ) (lemma-distr2 a b c f g )
+    lemma-distr1 a b c f g =  ( IsUniversalMapping.uniquness ( isUniversalMapping um ) a (F c)) (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
@@ -229,7 +226,7 @@
             (FMap U (FMap F' f))  o  ( η a ) 
        ≈⟨⟩
             (FMap U ((_* um)  (A [  η b  o f ])))   o  ( η a ) 
-       ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) a ( F b )  ⟩
+       ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
             (η b ) o f 
        ∎
     myIsNTrans : IsNTrans A A identityFunctor ( U ○  F' ) η
@@ -248,6 +245,27 @@
     F' = FunctorF A B U F η um
     ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b
     ε b = (_* um) ( id1 A (FObj U b))
+    lemma-nat1 :  (a b : Obj B) (f : Hom B a b ) -> 
+             A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] )  o η (FObj U a) ]
+                 ≈ A [ FMap U f o id1 A (FObj U a) ] ]
+    lemma-nat1 a b f = let open ≈-Reasoning (A) in
+       begin 
+          FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] )  o η (FObj U a) 
+       ≈⟨ car ( IsFunctor.distr ( isFunctor U ) ) ⟩
+          ( FMap U  ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) )  o η (FObj U a) 
+       ≈⟨ sym assoc  ⟩
+           FMap U  ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f )))  o η (FObj U a) 
+       ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) )  ⟩
+           FMap U  ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f )
+       ≈⟨ assoc  ⟩
+           (FMap U  ((um *) (id1 A (FObj U b))) o  η (FObj U b)) o FMap U f 
+       ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩
+           id1 A (FObj U b) o FMap U f 
+       ≈⟨ idL ⟩
+            FMap U f 
+       ≈⟨ sym idR ⟩
+          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
@@ -257,6 +275,8 @@
           ε 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)) ⟩
+          (_* um) ( A [ FMap U f o id1 A (FObj U a) ] )
        ≈⟨ {!!} ⟩
           f o  ((_* um) ( id1 A (FObj U a)))
        ≈⟨⟩