--- a/freyd2.agda	Mon Nov 13 12:39:43 2017 +0900
+++ b/freyd2.agda	Mon Nov 13 13:31:35 2017 +0900
@@ -89,7 +89,7 @@
          where open import Comma1 F G
 
 open Complete
-open IsInitialObject
+open HasInitialObject
 open import Comma1
 open CommaObj
 open LimitPreserve
@@ -182,7 +182,7 @@
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
-      → IsInitialObject  ( K A Sets * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
+      → HasInitialObject  ( K A Sets * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ f → unique f
@@ -278,7 +278,7 @@
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (U : Functor A (Sets {c₂}) )
      ( i : Obj ( K A Sets * ↓ U) )
-     (In : IsInitialObject ( K A Sets * ↓ U) i ) 
+     (In : HasInitialObject ( K A Sets * ↓ U) i ) 
        → Representable A U (obj i)
 UisRepresentable A U i In = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
@@ -370,7 +370,7 @@
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
      (i :  (b : Obj B) → Obj ( K A B b ↓ U) )
-     (In :  (b : Obj B) → IsInitialObject ( K A B b ↓ U) (i b) ) 
+     (In :  (b : Obj B) → HasInitialObject ( K A B b ↓ U) (i b) ) 
         where
 
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))