--- a/freyd2.agda	Tue Jun 13 22:53:44 2017 +0900
+++ b/freyd2.agda	Wed Jun 14 10:37:41 2017 +0900
@@ -154,7 +154,7 @@
                  ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t  ] ) x
              ≈⟨⟩
                 FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
-             ≈⟨⟩
+             ≈⟨⟩ -- FMap (Hom A b ) f g  = A [ f o g  ]
                 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
              ≈⟨  cdr idR ⟩
                 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) 
@@ -185,23 +185,6 @@
        preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
    } 
 
--- 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 {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 )
 
@@ -212,7 +195,42 @@
       (R : Representable A U a ) →
       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 → {!!}
+           initial =  λ b → initial0 b
          ; uniqueness =  λ b f → {!!}
-     }
+     } where
+         initial0com :  (b : Obj (K Sets A (FObj U a) ↓ U)) →
+              Sets [ Sets [ FMap U (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) o id1 Sets (FObj U a) ]
+                 ≈ Sets [ hom b o FMap (K Sets A (FObj U a)) (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) ] ]
+         initial0com b = let open ≈-Reasoning Sets in begin
+                   FMap U (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) o id1 Sets (FObj U a)
+             ≈⟨⟩
+                   FMap U (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) 
+             ≈⟨ {!!} ⟩
+                   hom b o FMap (K Sets A (FObj U a)) (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a))))
+             ∎ 
 
+         initial0 : (b : Obj (K Sets A (FObj U a) ↓ U)) →
+            Hom ((K Sets A (FObj U a)) ↓ U)
+              (record { obj = a ; hom = id1 Sets (FObj U a) }) b
+         initial0 b = record {
+                arrow =   TMap ( repr→ R ) (obj b) ( hom b (TMap ( repr← R ) a (id1 A a)))
+              ; comm = initial0com b }
+            
+
+-- 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 {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}  →　?
+    }
+