Mercurial > hg > Members > kono > Proof > category

changeset 565:6cf91ef84ca0

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, 24 Apr 2017 10:40:38 +0900
parents 40dfdb801061
children ecef5008cc17
files SetsCompleteness.agda
diffstat 1 files changed, 12 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 24 10:18:36 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 10:40:38 2017 +0900
@@ -245,13 +245,24 @@
               limit1 a t x = record {
                    snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x  )
                 } 
+              uniquness2 : {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 ]) →  (x : a )
+                     → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t {!!} x )  ≡ snequ1 (f x ) {!!}
+              uniquness2 = {!!}
               uniquness1 : {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 ]
               uniquness1 {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
                 ≡⟨⟩
                    record { snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x ) }
-                ≡⟨ ≡cong ( λ e → record { snequ1 =  λ {i} {j} f → e x } ) ?   ⟩
+                ≡⟨ ≡cong ( λ e → record { snequ1 =  λ {i} {j} f' → e i j f' x } ) (
+                        extensionality Sets  ( λ  i  →
+                           extensionality Sets  ( λ  j  →
+                               extensionality Sets  ( λ  f'  →
+                                   extensionality Sets  ( λ  x  → 
+                  elm-cong (  elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f' x )) (snequ1 (f x) f' ) {!!}  )
+                           )))
+                     ) ⟩
                    record { snequ1 = λ {i} {j} f' → snequ1 (f x ) f' }
                 ≡⟨⟩
                   f x