Mercurial > hg > Members > kono > Proof > category

changeset 560:ba9c6dbbe6cb

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:14:53 +0900
parents e8ab4fcfe033
children 2c0e168c832e
files SetsCompleteness.agda
diffstat 1 files changed, 43 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 10 03:13:28 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 10 10:14:53 2017 +0900
@@ -127,8 +127,8 @@
 
 SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g
 SetsIsEqualizer {c₂} a b f g = record { 
-               fe=ge  = fe=ge
-             ; k = k
+               fe=ge  = fe=ge { c₂ } {a} {b} {f} {g}
+             ; k = λ {d} h eq → k { c₂ } {a} {b} {f} {g} {d} h eq
              ; ek=h = λ {d} {h} {eq} → ek=h {c₂} {a} {b} {f} {g} {d} {h} {eq}
              ; uniqueness  = uniqueness
        } where
@@ -224,7 +224,7 @@
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
-             ; limit-uniqueness  =  λ {a t i }  → {!!} -- limit-uniqueness   {a} {t} {i}
+             ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
           }
        }  where
           a0 : Obj Sets
@@ -234,15 +234,16 @@
           comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
              → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
           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 =  {!!}
           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 ) {!!} x
+                snequ1 = λ {i} {j} f → k ( setprod t ) (comm3 {a} {x} t f ) x
             }
           t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ]
           t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
                  ( Sets [ TMap (Cone C I s Γ ) i o limit1 a t ]) x
-             -- ≡⟨⟩
-                 -- snmap ( record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f }  ) i
              ≡⟨⟩
                  TMap t i x
              ∎  ) where
@@ -250,4 +251,39 @@
                   open ≡-Reasoning
           limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} →
                 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
-          limit-uniqueness {a} {t} {f} cif=t =  {!!}
+          limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
+                  limit1 a t x
+             ≡⟨⟩
+                  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 
+                            )))
+                      ) ⟩
+                  record { snequ1 = λ {i} {j} f' → snequ1 (f x) f' }
+             ≡⟨⟩
+                  f x
+             ∎  ) 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' 
+                  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)
+                            ≡⟨⟩
+                               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 ( equ ( snequ1 (f x) (λ x → x ))) i'
+                                  ≡⟨  ≡cong ( λ f → f x ) cif=t   ⟩
+                                     TMap t i' x
+                               ∎ )))) ⟩
+                               record { snmap =  λ i' → snmap (equ (snequ1 (f x) f')) i' }
+                            ≡⟨⟩
+                               equ (snequ1 (f x) f')
+                            ∎  
+                     ) ⟩
+                            snequ1 (f x) f'
+                     ∎  
+