--- a/freyd2.agda	Thu Jun 08 19:48:02 2017 +0900
+++ b/freyd2.agda	Mon Jun 12 10:50:02 2017 +0900
@@ -18,6 +18,20 @@
 --
 
 -- A is Locally small
+
+----
+-- C is locally small i.e. Hom C i j is a set c₁
+--
+record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
+                : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+   field
+     hom→ : {i j : Obj C } →    Hom C i j →  I
+     hom← : {i j : Obj C } →  ( f : I ) →  Hom C i j
+     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f
+
+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
@@ -66,7 +80,6 @@
              ∎ )
 
 
--- {*}↓U has preinitial full subcategory iff U is representable
 
 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
    field
@@ -77,56 +90,50 @@
 
          repr→ : NTrans A (Sets {c₂}) U (HomA A b )
          repr← : NTrans A (Sets {c₂}) (HomA A b)  U
-         representable→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
-         representable←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
+         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)]
+
+open import freyd
 
--- HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →  (b : Obj A)
---       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
---       → LimitPreserve A I (Sets  {c₂}) ( HomA A b )
--- HpreseveLimit {_} { c₂} A b I =  record {
---        preserve = λ Γ limita → record {
---              limit = λ a t → limitu a Γ t limita
---              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
---              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
---        }
---    } where
---       limitu :   ( a : Obj Sets ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
---           Hom Sets a (FObj (HomA A b) (a0 limita))
---       limitu  = {!!}
---       t0f=tu :    { a : Obj  Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
---            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ]
---       t0f=tu  = {!!}
---       limit-uniquenessu :    { a : Obj Sets } → (Γ : Functor I A ) 
---            →   ( limita : Limit A I Γ  ) →
---           ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f :  Hom Sets a (FObj (HomA A b) (a0 limita)) ) 
---            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) )
---            →  Sets [ limitu a Γ t limita ≈ f ]
---       limit-uniquenessu = {!!}
+_↓_ :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
+    →  ( F G : Functor A B )
+    →  Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
+_↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
+         where open import Comma1 F G
 
 
+open import freyd
 
---
--- 
--- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
---       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
---      ( rep :  Representable A U b ) → LimitPreserve A I (Sets  {c₂}) U 
--- UpreseveLimit {_} { c₂} A U b I rep =  record {
---        preserve = λ Γ limita → record {
---              limit = λ a t → limitu a Γ t limita
---              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
---              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
---        }
---    } where
---       limitu :   ( a : Obj (Sets  {c₂}) ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
---           Hom Sets a (FObj U (a0 limita))
---       limitu  = {!!}
---       t0f=tu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
---            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
---       t0f=tu  = {!!}
---       limit-uniquenessu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) 
---            →   ( limita : Limit A I Γ  ) →
---           ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f :  Hom Sets a (FObj U (a0 limita)) ) 
---            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
---            →  Sets [ limitu a Γ t limita ≈ f ]
---       limit-uniquenessu = {!!}
--- 
+-- K{*}↓U has preinitial full subcategory then U is representable
+
+open SmallFullSubcategory
+open Complete
+open PreInitial
+
+data OneObject : Set where
+  * : OneObject
+
+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 = {!!}
+
+-- K{*}↓U has preinitial full subcategory if U is representable
+
+KUhasSFS : {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 = {!!}
+
+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 = {!!}