Mercurial > hg > Members > kono > Proof > category

changeset 557:9902722e1578

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
close
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Apr 2017 22:58:50 +0900
parents 6277ac99db37
children c2eb1a2570ce
files SetsCompleteness.agda
diffstat 1 files changed, 8 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun Apr 09 22:56:26 2017 +0900
+++ b/SetsCompleteness.agda	Sun Apr 09 22:58:50 2017 +0900
@@ -242,7 +242,14 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; snequ =   λ {i} {j} f → elem (TMap t i x) (comm2 t f )  }
-             ≡⟨ ? ⟩
+             ≡⟨ ≡cong2 ( λ x y →   record { snmap = λ i → x i  ; snequ = λ {i} {j} f → y x i j f }   ) 
+                 ( extensionality Sets  ( λ  i →   eq1  x i ) )
+                   ( extensionality Sets  ( λ  x'  → 
+                   ( extensionality Sets  ( λ  i  → 
+                     ( extensionality Sets  ( λ  j  → 
+                       ( extensionality Sets  ( λ  f'  → elm-cong (elem (x' i ) {!!} ) {!!}  (   eq1  x i   )
+                     ))))))))
+              ⟩ 
                   record {  snmap = λ i →  snmap  (f x ) i  ; snequ =  snequ (f x)  }
              ≡⟨⟩
                   f x