--- a/freyd2.agda	Mon Jun 12 16:35:34 2017 +0900
+++ b/freyd2.agda	Mon Jun 12 18:11:23 2017 +0900
@@ -109,19 +109,31 @@
 open LimitPreserve
 
 -- Representable Functor U preserve limit , so K{*}↓U is complete
+--
+--    HomA A b =  λ a → Hom A a b    : Functor A Sets
+--                                   : Functor Sets A
+
+UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
+      (comp : Complete A A) (b : Obj A ) 
+      (Γ : Functor I A) (limita : Limit A I Γ) →
+        IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b))
+UpreserveLimit0 A I comp b Γ lim = record {
+         limit = λ a t → limit1 a t
+       ; t0f=t = λ {a t i} → {!!}
+       ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!}
+    } where 
+      ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) → NTrans I A (K A I {!!}) Γ
+      ta a t = {!!}
+      limit1 :  (a : Obj Sets)  ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ))
+          →  Hom Sets a (FObj (HomA A b) (a0 lim))
+      limit1 a t = Sets [ FMap (HomA A b) (limit (isLimit lim) (FObj {!!} b) (ta a t )) o TMap {!!} b ]
+
 
 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-      (comp : Complete A A)
-      (U : Functor A (Sets) )
-      (a : Obj A )
-      (R : Representable A U a ) → LimitPreserve A I Sets U 
-UpreserveLimit A I comp U a R = record {
-       preserve =  λ Γ lim → record {
-             limit = λ a t → {!!}
-           ; t0f=t = λ {a t i} → ?
-           ; limit-uniqueness = λ {a} {t} {f} t0f=t → {!!}
-         }
-   }
+      (comp : Complete A A) (b : Obj A ) → LimitPreserve A I Sets (HomA A b) 
+UpreserveLimit A I comp b = record {
+       preserve = λ Γ lim → UpreserveLimit0 A I comp b Γ lim
+   } 
 
 -- K{*}↓U has preinitial full subcategory then U is representable
 --    K{*}↓U is complete, so it has initial object