--- a/freyd2.agda	Sun Jun 25 13:03:33 2017 +0900
+++ b/freyd2.agda	Mon Jun 26 17:18:23 2017 +0900
@@ -185,7 +185,7 @@
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
-      → HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
+      → HasInitialObject  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ b f → unique b f
@@ -247,21 +247,23 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong
 
+ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
+ub A U b x OneObj = x
+
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
      (U : Functor A (Sets {c₂}) )
-     (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A * ↓ U) )  
-     (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A * ↓ U) (SFSF SFS )) 
+     (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
+     (pi : Obj ( K (Sets) A * ↓ U) )
+     (PI : PreInitial ( K (Sets) A * ↓ U) {pi} (SFSF SFS)) 
        → Representable A U (obj (preinitialObj PI ))
-UisRepresentable A U SFS PI = record {
+UisRepresentable A U SFS pi PI = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
-        ; reprId→  = λ {y}  →　?
-        ; reprId←  = λ {y}  →　?
+        ; reprId→  = {!!}
+        ; reprId←  = {!!}
    } where
-      ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
-      ub b x OneObj = x
-      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
-      tmap1 b x =  arrow ( SFSFMap← SFS ( preinitialArrow PI ) )  
+      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
+      tmap1 b x =  arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub A U b x}) } ))  
       tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
       tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
       comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]