--- a/freyd2.agda	Mon Jun 12 10:50:02 2017 +0900
+++ b/freyd2.agda	Mon Jun 12 16:35:34 2017 +0900
@@ -17,8 +17,6 @@
 --    U ⋍ Hom (a,-)
 --
 
--- A is Locally small
-
 ----
 -- C is locally small i.e. Hom C i j is a set c₁
 --
@@ -31,7 +29,6 @@
 
 open Small
 
-
 postulate ≈-≡ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
 import Relation.Binary.PropositionalEquality
@@ -79,20 +76,21 @@
                 A [ g o x ]
              ∎ )
 
-
+-- Representable  U  ≈　Hom(A,-)
 
-record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
+record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
    field
          -- FObj U x  :  A  → Set
-         -- FMap U f  =  Set → Set
+         -- FMap U f  =  Set → Set (locally small)
          -- λ b → Hom (a,b) :  A → Set
          -- λ f → Hom (a,-) = λ b → Hom  a b    
 
-         repr→ : NTrans A (Sets {c₂}) U (HomA A b )
-         repr← : NTrans A (Sets {c₂}) (HomA A b)  U
-         reprId  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
-         reprId  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
+         repr→ : NTrans A (Sets {c₂}) U (HomA A a )
+         repr← : NTrans A (Sets {c₂}) (HomA A a)  U
+         reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A a) x )]
+         reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
 
+open Representable
 open import freyd
 
 _↓_ :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
@@ -101,39 +99,58 @@
 _↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
          where open import Comma1 F G
 
-
 open import freyd
-
--- K{*}↓U has preinitial full subcategory then U is representable
-
 open SmallFullSubcategory
 open Complete
 open PreInitial
+open HasInitialObject
+open import Comma1
+open CommaObj
+open LimitPreserve
 
-data OneObject : Set where
-  * : OneObject
+-- Representable Functor U preserve limit , so K{*}↓U is complete
+
+UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
+      (comp : Complete A A)
+      (U : Functor A (Sets) )
+      (a : Obj A )
+      (R : Representable A U a ) → LimitPreserve A I Sets U 
+UpreserveLimit A I comp U a R = record {
+       preserve =  λ Γ lim → record {
+             limit = λ a t → {!!}
+           ; t0f=t = λ {a t i} → ?
+           ; limit-uniqueness = λ {a} {t} {f} t0f=t → {!!}
+         }
+   }
+
+-- K{*}↓U has preinitial full subcategory then U is representable
+--    K{*}↓U is complete, so it has initial object
 
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
-      (U : Functor A (Sets) )
-      (SFS : SmallFullSubcategory ( K (Sets) {!!} {!!} ↓ U )) → 
-      (PI : PreInitial {!!} (SFSF SFS )) → Representable A U {!!}
-UisRepresentable = {!!}
+      (U : Functor A (Sets {c₂}) )
+      (a : Obj Sets )
+      (x : Obj ( K (Sets) A a ↓ U) )
+      ( init : HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A a ↓ U ) x )
+        → Representable A U (obj x)
+UisRepresentable A comp U a x init = record {
+         repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
+         ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
+         ; reprId→  = λ {y}  →　?
+         ; reprId←  = λ {y}  →　?
+    }
 
 -- K{*}↓U has preinitial full subcategory if U is representable
+--     if U is representable,  K{*}↓U has initial Object ( so it has preinitial full subcategory )
 
-KUhasSFS : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (U : Functor A (Sets) )
       (a : Obj A )
       (R : Representable A U a ) →
-      SmallFullSubcategory {!!}
-KUhasSFS = {!!}
+      HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A (FObj U a) ↓ U ) ( record  { obj = a ; hom = id1 Sets (FObj U a) } )
+KUhasInitialObj A comp U a R = record {
+           initial =  λ b → {!!}
+         ; uniqueness =  λ b f → {!!}
+     }
 
-KUhasPreinitial : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (comp : Complete A A)
-      (U : Functor A (Sets) )
-      (a : Obj A )
-      (R : Representable A U a ) →
-      PreInitial {!!} (SFSF (KUhasSFS A comp U a R ) )
-KUhasPreinitial = {!!}