Mercurial > hg > Members > kono > Proof > category

changeset 568:f3fb9061a8ca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
last one problem in SetCompleteness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Apr 2017 12:01:03 +0900
parents 9e727ce08b2c
children 25c18786fbdc
files SetsCompleteness.agda
diffstat 1 files changed, 11 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 24 11:48:35 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 12:01:03 2017 +0900
@@ -248,7 +248,17 @@
               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 ]) →  (f' : I → I ) →  (x : a ) 
                      →  equ (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t f' x)) ≡ equ (snequ1 (f x) f')
-              uniquness2 cif=t f' x = refl 
+              uniquness2 {a} {t} {f} cif=t f' x = begin
+                  record { snmap = λ i₁ → TMap t i₁ x }
+                ≡⟨   ≡cong ( λ g → record { snmap = λ i → g i  } ) (  extensionality Sets  ( λ  i  →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
+                  record { snmap = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
+                ≡⟨⟩
+                  record { snmap = λ i →   snmap (equ (snequ1 (f x) {i} {i} (λ x → x )) ) i }
+                ≡⟨ {!!}  ⟩
+                  record { snmap = λ i₁ →  snmap (equ (snequ1 (f x) f')) i₁  }
+                ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
               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