--- a/freyd.agda	Sun Jan 05 23:37:12 2014 +0900
+++ b/freyd.agda	Mon Jan 06 00:46:48 2014 +0900
@@ -41,12 +41,14 @@
 
 open NTrans
 open Limit
+open SmallFullSubcategory
+open PreInitial
 
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
       (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
       (SFS : SmallFullSubcategory A F FMap← ) → 
-      (PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
+      (PI : PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
           → HasInitialObject A a0
 initialFromPreInitialFullSubcategory A F  FMap← lim SFS PI {a0} {u} = record {
       initial = λ a → limit (lim F {a} {u a} ) a0 (u a0) ; 
@@ -59,7 +61,15 @@
              ≈↑⟨ limit-uniqueness (lim F) ( λ {i} →
              begin
                   TMap (u a) i o f 
-             ≈⟨ ? ⟩
+             ≈⟨ cdr {!!} ⟩
+                  TMap (u a) i o ( preinitial PI {a} {i} o (limit (lim F {FObj F i } {u {!!} }) a0 ( u a0 ) ) )
+             ≈⟨ cdr {!!} ⟩
+                  TMap (u a) i o ( preinitial PI {a} {i} o TMap (u a0) i )
+             ≈⟨ assoc  ⟩
+                  ( TMap (u a) i o  preinitial PI {a} {i} ) o TMap (u a0) i 
+             ≈⟨ {!!} ⟩
+                  id1 A (FObj F i) o TMap (u a0) i 
+             ≈⟨ idL  ⟩
                   TMap (u a0) i
              ∎ 
              )⟩