--- a/freyd.agda	Sun Jan 05 19:02:29 2014 +0900
+++ b/freyd.agda	Sun Jan 05 19:16:18 2014 +0900
@@ -20,11 +20,28 @@
       full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
       full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]
 
-record PreInitial-SmallFullSubcategory {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 )
+-- pre-initial
+
+record PreInitialSmallFullSubcategory {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 }
       (SFS : SmallFullSubcategory A F FMap← ) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      pre-initial : ∀{  a : Obj A } → { a' : Obj A } →  Hom A ( FObj F a' ) a 
-      uniqueness  : ∀{  a : Obj A } → { a' : Obj A } →  ( f' : Hom A ( FObj F a' ) a ) →
-          A [ f'  ≈  pre-initial {a} {a'} ]
+      preinitial : ∀{  a : Obj A } → { b : Obj A } →  Hom A ( FObj F b ) a 
+      uniqueness  : ∀{  a : Obj A } → { b : Obj A } →  ( f : Hom A ( FObj F b ) a ) →
+          A [ f  ≈  preinitial {a} {b} ]
+
+-- initial object
 
+record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+   field
+      initial :  ( a : Obj A ) →  Hom A i a
+      uniqueness  : ( a : Obj A ) →  ( f : Hom A i a ) → A [ f ≈  initial a ]
+
+
+-- A has initial object if it has PreInitial-SmallFullSubcategory
+
+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 )
+      (SFS : SmallFullSubcategory A F FMap← ) → 
+      (PreInitialSmallFullSubcategory A SFS ) → { i : Obj A } → HasInitialObject A i
+initialFromPreInitialFullSubcategory A F  FMap← SFS PI = {!!}