# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490692215 -32400
# Node ID beac7b0786cbad0eee8ab0653ba0027205fd5c38
# Parent  b035cd3be525943f9386fb3061ebb072ab7a28fa
fix ...

diff -r b035cd3be525 -r beac7b0786cb SetsCompleteness.agda
--- a/SetsCompleteness.agda	Tue Mar 28 11:49:35 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 18:10:15 2017 +0900
@@ -151,7 +151,7 @@
    field
      small→ : Obj C → I
      small← : I → Obj C
-     small-iso : { i : I } → small→ ( small← i ) ≡ i
+     small-iso : { x : Obj C  } → Hom C (small← ( small→ x ))  x
      shom→ : {i j : Obj C  } →    Hom C i j →  I → I 
      shom← : {i j : I } →  ( f : I → I ) →  Hom C ( small←  i  ) (  small←  j )
      shom-iso : {i j : I } →  ( f : Hom C ( small←  i  ) (  small←  j ) ) →  C [ shom← ( shom→ f )  ≈ f ]
@@ -169,15 +169,18 @@
 
 record slim   { c₂ }  { I :  Set  c₂ } ( sobj :  I →  Set  c₂ ) 
      ( smap : { i j :  I  }  → (f : I → I )→  sobj i → sobj j ) : Set  c₂ where
+   field 
+        slim-obj : ( i : I ) → sobj i
 
+open slim
 
 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 = record { 
-               TMap = λ i → {!!}
-             ; isNTrans = record { commute = {!!} } 
+               TMap = λ i →  Sets [ proj i o e ]  
+             ; isNTrans = record { commute = comm1 } 
            }
          ; isLimit = record {
                limit  = {!!}
@@ -185,11 +188,22 @@
              ; limit-uniqueness  = {!!}
            }
        }  where
-          eqa : {i j : Obj Sets} (f : Hom Sets i j) → sequ (Obj Sets) (Obj Sets) {!!} {!!}         --  {!!} {!!} (FMap Γ f o  proj i) ( proj j ) 
-          eqa f = {!!}
-          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets (slim  {!!} {!!} )) i ) (iproduct (slim  {!!} {!!} ) (λ I → {!!} (slim  {!!} {!!} )))
-          e i =  λ x → record { pi1  = λ j →  {!!} }
-          proj :  (i : Obj Sets) → ( prod : iproduct (slim   {!!} {!!} ) (λ i → {!!} )) → {!!}
-          proj i prod =  {!!}
-          comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → {!!}
-          comm1 {a} {b} {f} = {!!} 
+          a0 : Obj Sets
+          a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
+          iid :  {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
+          iid {i} = FMap Γ ( small-iso s ) 
+          e  :  Hom Sets a0 (iproduct I (λ j → ΓObj s Γ j))
+          e  =  λ x → record { pi1  = λ j →  slim-obj x j }
+          proj :  (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i
+          proj i prod = iid (  pi1 prod ( small→ s i )  )
+          comm1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈
+                Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+          comm1 {a} {b} {f} = extensionality Sets  ( λ  x → begin
+                 ? 
+             ≡⟨ {!!}  ⟩
+                {!!}
+             ∎ )  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+