Mercurial > hg > Members > kono > Proof > category

changeset 556:6277ac99db37

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
give up this approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Apr 2017 22:56:26 +0900
parents 91d065bcfdc0
children 9902722e1578
files SetsCompleteness.agda
diffstat 1 files changed, 3 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}