--- a/freyd.agda	Fri Jun 30 21:52:14 2017 +0900
+++ b/freyd.agda	Fri Jun 30 23:36:54 2017 +0900
@@ -34,7 +34,7 @@
 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 ]
+      uniqueness  : { a : Obj A } →  ( f : Hom A i a ) → A [ f ≈  initial a ]
 
 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
 
@@ -53,7 +53,7 @@
       (PI : PreInitial A  (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
-      uniqueness  = λ a f → lemma1 a f
+      uniqueness  = λ {a} f → lemma1 a f
     } where
       F : Functor A A 
       F = SFSF SFS