Mercurial > hg > Members > kono > Proof > category

changeset 559:e8ab4fcfe033

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 10 Apr 2017 03:13:28 +0900
parents c2eb1a2570ce
children ba9c6dbbe6cb
files SetsCompleteness.agda
diffstat 1 files changed, 5 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 10 02:10:37 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 10 03:13:28 2017 +0900
@@ -224,17 +224,19 @@
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
-             ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
+             ; limit-uniqueness  =  λ {a t i }  → {!!} -- limit-uniqueness   {a} {t} {i}
           }
        }  where
           a0 : Obj Sets
           a0 =  snequ  (ΓObj s Γ) (ΓMap s Γ) 
+          setprod : {a : Obj Sets} → NTrans C Sets (K Sets C a) Γ → (x : a ) → snproj  (ΓObj s Γ) (ΓMap s Γ)
+          setprod t x  = record { snmap = λ i → TMap t i x }
           comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
              → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
           comm2 {a} {x} t f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 a t = λ ( x : a ) →  record {
-                snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( comm2 t f ) 
+                snequ1 = λ {i} {j} f → k ( setprod t ) {!!} x
             }
           t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ]
           t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
@@ -248,26 +250,4 @@
                   open ≡-Reasoning
           limit-uniqueness : {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 ]
-          limit-uniqueness {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 }  ) ( comm2 t f ) }
-             ≡⟨ ≡cong ( λ se → record { snequ1 = λ {i} {j} f → se i j f  }) 
-                  (  extensionality Sets  ( λ  i  →  ( extensionality Sets  ( λ  j  →  ( extensionality Sets  ( λ  f'  → 
-                      sncong x f' i  {!!} (  ≡cong ( λ f → f x ) cif=t    )
-                  ))))))
-               ⟩
-                  record {  snequ1 =  snequ1 (f x)  }
-             ≡⟨⟩
-                  f x
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-                  sncong :  (x : a) → (f' : I → I ) → ( i : Obj C ) → ( se : snequ (ΓObj s Γ) (ΓMap s Γ) ) 
-                       →  snmap ( equ ( snequ1 se {i} {i} (λ x → x )) ) i  ≡  TMap t i x
-                       → elem (record { snmap = λ i → TMap t i x }) (comm2 t f') ≡ snequ1 (f x) f'
-                  sncong x f' i se eq = {!!}
-
-
-
-
+          limit-uniqueness {a} {t} {f} cif=t =  {!!}