--- a/freyd.agda	Sun Jun 25 13:03:33 2017 +0900
+++ b/freyd.agda	Mon Jun 26 17:18:23 2017 +0900
@@ -1,8 +1,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 
-module freyd {c₁ c₂ ℓ : Level} 
-  where
+module freyd where
 
 open import cat-utility
 open import HomReasoning
@@ -24,10 +23,11 @@
 -- pre-initial
 
 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+      {preini : Obj A} (F : Functor A A)  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      preinitialObj : Obj A 
-      preinitialArrow : ∀{  a : Obj A } →  Hom A ( FObj F (preinitialObj)) a 
+      preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj F preini) a 
+   preinitialObj : Obj A 
+   preinitialObj = preini
 
 -- initial object
 
@@ -50,7 +50,7 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (SFS : SmallFullSubcategory A ) → 
-      (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
+      (PI : PreInitial A {limit-c comp (SFSF SFS)} (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f