# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1510547495 -32400
# Node ID 7a6ee564e3a8ae1246d061cefdd9a562fd2ab84e
# Parent  2043f7fd427363646d3eceda2d78d52be075ceb4
fix

diff -r 2043f7fd4273 -r 7a6ee564e3a8 cat-utility.agda
--- a/cat-utility.agda	Mon Nov 13 12:39:43 2017 +0900
+++ b/cat-utility.agda	Mon Nov 13 13:31:35 2017 +0900
@@ -356,11 +356,6 @@
              ; t0 =  LimitNat I A C Γ (a0 limita ) (t0 limita) G
              ; isLimit = preserve Γ limita }
 
-        record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' )
-                : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
-          field
-             climit :  ( Γ : Functor I A ) → Limit I A Γ 
-
         record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
@@ -381,7 +376,7 @@
 
 -- initial object
 
-        record IsInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+        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 ]
@@ -389,5 +384,5 @@
         record InitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
           field
              initialObject :  Obj A 
-             isInitialObject :  IsInitialObject A initialObject
+             hasInitialObject :  HasInitialObject A initialObject
 
diff -r 2043f7fd4273 -r 7a6ee564e3a8 freyd.agda
--- a/freyd.agda	Mon Nov 13 12:39:43 2017 +0900
+++ b/freyd.agda	Mon Nov 13 13:31:35 2017 +0900
@@ -48,7 +48,7 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (SFS : FullSubcategory A ) → 
-      (PI : PreInitial A  (FSF SFS )) → IsInitialObject A (limit-c comp (FSF SFS))
+      (PI : PreInitial A  (FSF SFS )) → HasInitialObject A (limit-c comp (FSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ {a} f → lemma1 a f
diff -r 2043f7fd4273 -r 7a6ee564e3a8 freyd2.agda
--- 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)))