# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489897692 -32400
# Node ID b9c086bda3cc493c24049089818339f988038a27
# Parent  5eb4b69bf541002192283034af5b1548e8ec0bab
fix

diff -r 5eb4b69bf541 -r b9c086bda3cc SetsCompleteness.agda
--- a/SetsCompleteness.agda	Sun Mar 19 11:14:49 2017 +0900
+++ b/SetsCompleteness.agda	Sun Mar 19 13:28:12 2017 +0900
@@ -122,7 +122,19 @@
            ek=h {d} {h} {eq} = refl 
            uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h eq  ≈ k' ]
-           uniqueness  {d} refl =  extensionality Sets ( λ x → {!!} )
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets ( λ x →  
+              begin
+                k h fh=gh x
+              ≡⟨ {!!} ⟩
+                 elem  (h x) ( ≡-cong ( λ y → y x ) fh=gh  )
+              ≡⟨ {!!} ⟩
+                 elem  (equ (k' x)) {!!}
+              ≡⟨ {!!} ⟩
+                 k' x
+              ∎  
+             ) where
+                  open  import  Relation.Binary.PropositionalEquality 
+                  open ≡-Reasoning 
 
 
 open Functor
@@ -163,19 +175,19 @@
 
 open Slimit
 
-SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
-SetsLimit { c₂}  = record { 
-           a0 =  Slimit (Obj Sets) {!!} ΓMap
-         ; t0 = record { 
-               TMap = λ i → λ lim → s-t0 lim {!!} 
-             ; isNTrans = record { commute = {!!} } 
-           }
-         ; isLimit = record {
-               limit  = {!!}
-             ; t0f=t = {!!}
-             ; limit-uniqueness  = {!!}
-           }
-       }  where
+-- SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
+-- SetsLimit { c₂}  = record { 
+--            a0 =  Slimit (Obj Sets) {!!} ΓMap
+--          ; t0 = record { 
+--                TMap = λ i → λ lim → s-t0 lim {!!} 
+--              ; isNTrans = record { commute = {!!} } 
+--            }
+--          ; isLimit = record {
+--                limit  = {!!}
+--              ; t0f=t = {!!}
+--              ; limit-uniqueness  = {!!}
+--            }
+--        }  where
 --           comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → s-t0 lim ? ) ] ≈
 --                        Sets [ (λ lim → s-t0 lim ?) o FMap (K Sets Sets (Slimit (Obj Sets) ΓObj (λ {a} {b} → ΓMap))) f ] ]
   --           comm1 {a} {b} {f} = {!!}