--- a/SetsCompleteness.agda	Fri Mar 17 11:53:53 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 17 19:55:51 2017 +0900
@@ -54,36 +54,60 @@
 open Functor
 open NTrans
 
-record Slimit  { c₂ }  (I :  Set  c₂ ) ( ΓObj  : I → Set  c₂ ) 
-          ( ΓMap : ( f : I → I ) →  Set  c₂   →  Set  c₂   )  : Set  c₂ where
-     field
-        sobj :  I
-        bb :  ΓObj  sobj
-        cc :  I → I
-        ec :  ΓMap cc I
-        dc :  ΓObj  sobj → I
+record ΓObj   { c₂ }  (x :  Set  c₂ ) : Set  c₂ where
+   field
+     obj :  x
+
+open ΓObj
+
+record ΓMap   { c₂ }  {a b :  Set  c₂ } ( f : a → b )  : Set  c₂ where
+   field
+     map : ΓObj a → ΓObj b
+
+open ΓMap
+
+
+record Slimit  { c₂ }  ( sobj : Set  c₂ →  Set  c₂ ) (smap :  {a b :  Set  c₂ } ( f : a → b ) →  Set  c₂ )
+           : Set  c₂ where
+--    field 
+--       aap : ΓObj slim  
+--       ap : ΓObj slim  → ΓObj slim
+--       hoge : sobj  slim
+--       hoge1 : smap {slim} {slim} ( λ x → x )
+
+record ΓTMap   { c₂ }  (a :  Set  c₂ )   : Set  c₂ where
+   field
+     tmap : a →  Slimit  ΓObj  ΓMap → ΓObj a
+
+open ΓTMap
+
+
+--       sobj  :  S
+--       smap  :  fobj  S
+--       hoge  :  ΓObj S
+
+--        bb :  ΓObj  I
+--        cc :  I → I
 
 open Slimit
 
-SetsLimit : { c₂ : Level} 
-          ( I :  Set  c₂ ) ( ΓObj'  : I → Set  c₂ )( ΓMap' :   {  f : I → I } →  Set  c₂   →  Set  c₂ ) 
-          ( ΓObj :  Obj Sets → Obj Sets ) ( ΓMap :  {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B ))
-          ( Γ : IsFunctor  (Sets { c₂}) (Sets { c₂}) ΓObj ΓMap ) 
-        →  Limit Sets Sets ( record { FObj =  ΓObj ; FMap =  ΓMap ; isFunctor = Γ } )
-SetsLimit { c₂} I ΓObj' ΓMap'  ΓObj ΓMap Γ = record { 
-           a0 =  Slimit  I  ΓObj'  ΓMap'
-         ; t0 = record { TMap = tmap ; isNTrans = record { commute = tcommute } }
+tmp : { c₂ : Level}   {a b :  Set  c₂ } → (f : a → b  ) → ΓMap f
+tmp {a} {b} f =  record { map = λ aobj →  record { obj = f ( obj aobj ) } }
+
+ttmp : {c₂ : Level}   (A  :  Set  c₂ ) →   ΓTMap A
+ttmp  A = record { tmap  =  λ a slim → record { obj = a } }
+
+SetsLimit :  { c₂ : Level} (e : Set  c₂)   ( Γ : IsFunctor  (Sets { c₂}) (Sets { c₂}) ΓObj ( λ f →  map (tmp f ) ))
+        →  Limit Sets Sets ( record { FObj =  ΓObj ; FMap = ( λ f →  map (tmp f )) ; isFunctor = Γ } )
+SetsLimit { c₂} e   Γ = record { 
+           a0 =  Slimit   ΓObj  ΓMap  
+         ; t0 = record { TMap = λ i → {!!} ; isNTrans = record { commute = {!!} } }
          ; isLimit = record {
                limit  = {!!}
              ; t0f=t = {!!}
              ; limit-uniqueness  = {!!}
            }
-       } where
-          tmap :  (a : Obj Sets) → Hom Sets (Slimit  I {!!}  {!!}) (ΓObj a)
-          tmap  a _ = {!!}
-          tcommute :   {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap  b o id1 Sets (Slimit I {!!} {!!})  ] ]
-          tcommute {a} {b} {f} = {!!}
-
-
-
-
+       } where  
+            tmap0 :  (a : Obj Sets) → Hom Sets (FObj (K Sets Sets (  Slimit   ΓObj  ΓMap)) a) (ΓObj a)
+            tmap0 a oa =  tmap ( ttmp a ) ? oa
+