# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1494485914 -32400
# Node ID 59c3de1c4043f40ba55a6440f39f59e30810dd2d
# Parent  f0f51681776240e3024e60604ed0899e0f04f2a2
on oging ...

diff -r f0f516817762 -r 59c3de1c4043 SetsCompleteness.agda
--- a/SetsCompleteness.agda	Thu May 11 14:49:17 2017 +0900
+++ b/SetsCompleteness.agda	Thu May 11 15:58:34 2017 +0900
@@ -181,6 +181,7 @@
       :  Set   c₂  where
    field 
        slequ : ( e : OC → sproduct OC sobj  )  (i j : OC) (f :  I → I  ) → sequ OC (sobj j) (λ x →  smap f (proj (e x) i) ) (λ x → proj (e x) j )
+       slprod :  sproduct OC  sobj 
 
 open slim
 
@@ -188,10 +189,9 @@
 open NTrans
 
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
-    → ( prod :  Set  c₁ → sproduct (Obj C) (ΓObj s Γ) )
     → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  ) (sproduct (Obj C) (ΓObj s  Γ)  ) )
     → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
-Cone C I s  Γ prod e  =  record {
+Cone C I s  Γ e  =  record {
                TMap = λ i →  λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s  Γ)}  {FObj Γ i}
                      {λ x → proj x i} {λ x → proj x i} (elem (e se ) refl )) i
              ; isNTrans = record { commute = commute1 }
@@ -218,3 +218,21 @@
                   open ≡-Reasoning
 
 
+SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
+    → Limit Sets C Γ
+SetsLimit { c₂} C I s Γ = record { 
+           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
+         ; t0 = Cone C I s Γ ( λ se → slprod se )
+         ; isLimit = record {
+               limit  = limit1
+             ; t0f=t = λ {a t i } → {!!}
+             ; limit-uniqueness  =  λ {a t i }  → {!!}
+          }
+       }  where
+          comm2 : ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  )  (sproduct (Obj C) (ΓObj s  Γ)  ) ) {i j : Obj C } ( f : I → I ) 
+             → (p : sproduct (Obj C) (ΓObj s  Γ) )
+             → ΓMap s Γ f (proj p i) ≡ proj p j
+          comm2  e {i} {j} f p = {!!}
+          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
+          limit1 a t = λ x →  record { slequ = λ e i j f →　elem i {!!}
+               ; slprod = record { proj = λ i → TMap t i x } }