# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489668190 -32400
# Node ID 01a0dda67a8bd0a787cf1727ec7f0909c97691cd
# Parent  61daa68a70c4313f99aea7d0417f84da93f062bc
on going ..

diff -r 61daa68a70c4 -r 01a0dda67a8b freyd2.agda
--- a/freyd2.agda	Thu Mar 16 10:26:30 2017 +0900
+++ b/freyd2.agda	Thu Mar 16 21:43:10 2017 +0900
@@ -66,42 +66,45 @@
              ∎ )
 
 
-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 = {!!}
+-- {*}↓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
+         -- FObj U x  :  A  → Set
+         -- FMap U f  =  Set → Set
+         -- λ 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
+         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)]
+
+-- 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 = {!!}
 
 
 
--- 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
---          -- FObj U x  :  A  → Set
---          -- FMap U f  =  Set → Set
---          -- λ 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
---          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)]
 --
 -- 
 -- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)