# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1509355116 -32400
# Node ID 959954fc29f86197ce99275d9d8c9890dae399c6
# Parent  99065a1e56eaf96ccd5519a7580d3313f9d29d7a
fix

diff -r 99065a1e56ea -r 959954fc29f8 freyd.agda
--- 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