Mercurial > hg > Members > kono > Proof > category

changeset 561:2c0e168c832e

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 Mon, 10 Apr 2017 10:48:50 +0900
parents ba9c6dbbe6cb
children 14483d9d604c
files SetsCompleteness.agda
diffstat 1 files changed, 9 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 10 10:14:53 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 10 10:48:50 2017 +0900
@@ -236,7 +236,7 @@
           comm2 {a} {x} t f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
           comm3 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
               → Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap x₁ i)) o setprod t ] ≈ Sets [ (λ x₁ → snmap x₁ j) o setprod t ] ]
-          comm3 {a} {x} t f =  {!!}
+          comm3 {a} {x} t f =  IsNTrans.commute (isNTrans t )
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 a t = λ ( x : a ) →  record {
                 snequ1 = λ {i} {j} f → k ( setprod t ) (comm3 {a} {x} t f ) x
@@ -256,7 +256,8 @@
              ≡⟨⟩
                   record { snequ1 = λ {i} {j} f' → k ( setprod t ) (comm3 {a} {x} t f' ) x }
              ≡⟨ ≡cong ( λ ff → record { snequ1 = λ {i} {j} f' → ff i j f' }) (  
-                            extensionality Sets  ( λ  i  →  extensionality Sets  ( λ  j  →  extensionality Sets  ( λ  f'  → k-cong {i} {j} f' x 
+                            extensionality Sets  ( λ  i  →  extensionality Sets  ( λ  j  →  extensionality Sets  ( λ  f'  
+                                → k-cong {i} {j} f' x 
                             )))
                       ) ⟩
                   record { snequ1 = λ {i} {j} f' → snequ1 (f x) f' }
@@ -265,16 +266,19 @@
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-                  k-cong : { i j : Obj C } ( f' : I → I ) ( x : a ) →   k ( setprod t ) (comm3 {a} {x} t f' ) x ≡  snequ1 (f x) f' 
+                  snmap-cong : ( e : snequ  (ΓObj s Γ) (ΓMap s Γ) ) {i : Obj C } { f g : I → I } 
+                        →   snmap ( equ ( snequ1 e  f)) i ≡  snmap ( equ ( snequ1 e  g)) i
+                  snmap-cong e {i} =  ≡cong ( λ s → snmap s i ) refl
+                  k-cong : { i j : Obj C } ( f' : I → I )  ( x : a ) →   k ( setprod t ) (comm3 {a} {x} t f' ) x ≡  snequ1 (f x) f' 
                   k-cong {i} {j} f' x = begin 
                             k ( setprod t ) (comm3 {a} {x} t f' ) x
                         ≡⟨ elm-cong (k ( setprod t ) (comm3 {a} {x} t f' ) x ) ( snequ1 (f x) f' )  ( begin 
-                               equ (k (setprod t) (comm3 t f') x)
+                               equ (k (setprod t) (comm3 {a} {x} t f') x)
                             ≡⟨⟩
                                record { snmap =  λ i' → TMap t i' x }
                             ≡⟨ ≡cong ( λ s → record { snmap = λ i' → s i' } ) ( extensionality Sets  ( λ  i'  → ( sym ( begin
                                     snmap ( equ ( snequ1 (f x) f')) i'
-                                  ≡⟨ ? ⟩
+                                  ≡⟨ snmap-cong (f x) ⟩
                                     snmap ( equ ( snequ1 (f x) (λ x → x ))) i'
                                   ≡⟨  ≡cong ( λ f → f x ) cif=t   ⟩
                                      TMap t i' x