Mercurial > hg > Members > kono > Proof > category

changeset 46:5d1b0fd2ad21

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Functor cong done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jul 2013 02:57:11 +0900
parents 659b8a21caf7
children 0124e3c971e5
files universal-mapping.agda
diffstat 1 files changed, 28 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Tue Jul 23 01:45:56 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 02:57:11 2013 +0900
@@ -6,6 +6,9 @@
 
 open Functor
 
+id1 :   ∀{c₁ c₂ ℓ  : Level} (A : Category c₁ c₂ ℓ)  (a  : Obj A ) →  Hom A a a
+id1 A a =  (Id {_} {_} {_} {A} a)
+
 record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Obj A -> Obj B )
@@ -38,9 +41,9 @@
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
        adjoint1 :   { b' : Obj B } ->
-                     A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ Id {_} {_} {_} {A} (FObj U b') ]
+                     A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ id1 A (FObj U b') ]
        adjoint2 :   {a' : Obj A} ->
-                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ Id {_} {_} {_} {B} (FObj F a') ]
+                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ id1 B (FObj F a') ]
 
 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
@@ -145,23 +148,38 @@
        } where
     myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b)
     myFMap f = (_* um)  (A [  η (Category.cod A f )   o f ]) 
-    lemma-id-1 :  {a : Obj A} ->  A [ A [ FMap U (Id {_} {_} {_} {B} (F a))  o  η a ]  ≈ (A [ (η a) o (Id {_} {_} {_} {A} a) ]) ]
-    lemma-id-1 {a} = let open ≈-Reasoning (A) in
+    lemma-id1 :  {a : Obj A} ->  A [ A [ FMap U (id1 B (F a))  o  η a ]  ≈ (A [ (η a) o (id1 A a) ]) ]
+    lemma-id1 {a} = let open ≈-Reasoning (A) in
        begin
-            A [ FMap U (Id {_} {_} {_} {B} (F a))  o  η a ] 
+           FMap U (id1 B (F a))  o  η a 
        ≈⟨ ( car ( IsFunctor.identity ( isFunctor U )))  ⟩
-            A [ (Id {_} {_} {_} {A} (FObj U ( F a )) ) o  η a ] 
+           id (FObj U ( F a )) o  η a 
        ≈⟨ idL  ⟩
            η a
        ≈⟨ sym idR  ⟩
-           (A [ (η a) o (Id {_} {_} {_} {A} a) ]) 
+           η a o id a
        ∎
-    lemma-id :  {a : Obj A} →  B [ ( (_* um) (A [ (η a) o (Id {_} {_} {_} {A} a)] )) ≈ (Id {_} {_} {_} {B} (F 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 (Id {_} {_} {_} {A} a)] )) ((Id {_} {_} {_} {B} (F a))) lemma-id-1
+              a (F a)  ((A [ (η a) o (id1 A a)] )) ((id1 B (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)  ⟩
+          η 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-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
     myIsFunctor : IsFunctor A B F myFMap
     myIsFunctor =
-      record { ≈-cong   = {!!}
+      record { ≈-cong   = lemma-cong
              ; identity = lemma-id
              ; distr    = {!!}
              }