--- a/freyd2.agda	Mon Jun 12 23:25:39 2017 +0900
+++ b/freyd2.agda	Tue Jun 13 10:15:24 2017 +0900
@@ -114,10 +114,10 @@
 --                                   : Functor Sets A
 
 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-      (comp : Complete A A) (b : Obj 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 {c₁} {c₂} {ℓ} A I comp b Γ lim = record {
+UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record {
          limit = λ a t → ψ a t
        ; t0f=t = λ {a t i} → t0f=t0 a t i
        ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!}
@@ -150,13 +150,25 @@
       ψ X t x = FMap (HomA A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
       t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I)
            → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ]
-      t0f=t0 = {!!}
+      t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
+                 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t  ] ) x
+             ≈⟨⟩
+                (FMap (HomA A b) ( TMap (t0 lim) i)) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
+             ≈⟨ {!!} ⟩
+                FMap (HomA A b) (A [ TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) ])  (id1 A b )
+             ≈⟨ ? ⟩
+                FMap (HomA A b) (TMap t i x)  (id1 A b )
+             ≈⟨ {!!} ⟩
+                 {!!} o TMap t i x
+             ≈⟨ idL ⟩
+                 TMap t i x
+             ∎  ))
 
 
 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-      (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
+       (b : Obj A ) → LimitPreserve A I Sets (HomA A b) 
+UpreserveLimit A I b = record {
+       preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
    } 
 
 -- K{*}↓U has preinitial full subcategory then U is representable