# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1491746186 -32400
# Node ID 6277ac99db37467aa0ebdecb3b591c9d7157703e
# Parent  91d065bcfdc07f0dd9b09ae6f88b99c5229f1de9
give up this approach

diff -r 91d065bcfdc0 -r 6277ac99db37 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Sun Apr 09 21:20:25 2017 +0900
+++ b/SetsCompleteness.agda	Sun Apr 09 22:56:26 2017 +0900
@@ -242,14 +242,7 @@
                   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 (TMap t i x ) {!!}) ? {!!}
-                     ))))))))
-              ⟩ 
+             ≡⟨ ? ⟩
                   record {  snmap = λ i →  snmap  (f x ) i  ; snequ =  snequ (f x)  }
              ≡⟨⟩
                   f x
@@ -258,5 +251,7 @@
                   open ≡-Reasoning
                   eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
                   eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
+                  eq2 : ( i j : Obj C ) (x' : Obj C → FObj Γ {!!} )   → (f' : I → I )  →   ΓMap s Γ f' (x' i) ≡ x' j
+                  eq2 = {!!}