--- a/freyd.agda	Mon Oct 30 18:14:41 2017 +0900
+++ b/freyd.agda	Mon Oct 30 18:18:36 2017 +0900
@@ -30,11 +30,11 @@
       preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj F preinitialObj ) a 
 
 -- 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 ]
+--   now in cat-utility
+-- 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 complete catagory has initial object if it has PreInitial-SmallFullSubcategory