--- a/freyd2.agda	Fri Jun 30 21:52:14 2017 +0900
+++ b/freyd2.agda	Fri Jun 30 23:36:54 2017 +0900
@@ -188,7 +188,7 @@
       → 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
+         ; uniqueness =  λ f → unique f
      } where
          commaCat : Category  (c₂ ⊔ c₁) c₂ ℓ
          commaCat = K Sets A * ↓ Yoneda A a
@@ -222,9 +222,9 @@
             → Sets [ Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ]
                ≈ Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ] 
          comm-f b f = comm f
-         unique : (b : Obj (K Sets A * ↓ Yoneda A a))  (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
+         unique : {b : Obj (K Sets A * ↓ Yoneda A a)}  (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
                 → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ]
-         unique b f = let open ≈-Reasoning A in begin
+         unique {b} f = let open ≈-Reasoning A in begin
                 arrow f
              ≈↑⟨ idR ⟩
                 arrow f o id1 A a
@@ -258,27 +258,21 @@
 
 -- if K{*}↓U has initial Obj, U is representable
 
-UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( comp : Complete A A )
+UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (U : Functor A (Sets {c₂}) )
-     (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
-     (PI : PreInitial ( K (Sets) A * ↓ U)  (SFSF SFS)) 
-       → Representable A U (obj (preinitialObj PI ))
-UisRepresentable A comp U SFS PI = record {
+     ( i : Obj ( K (Sets) A * ↓ U) )
+     (In : HasInitialObject ( K (Sets) A * ↓ U) i ) 
+       → Representable A U (obj i)
+UisRepresentable A U i In = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
         ; reprId→  = {!!}
         ; reprId←  = {!!}
    } where
-      pi : Obj ( K (Sets) A * ↓ U) 
-      pi = preinitialObj PI
-      pihom : Hom Sets (FObj (K Sets A *) (obj pi)) (FObj U (obj pi))
-      pihom = hom pi
       ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
       ub b x OneObj = x
       ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U)
       ob b x = record { obj = b ; hom = ub b x}
-      piArrow : (b : Obj ( K Sets A * ↓ U)) → Hom ( K Sets A * ↓ U) pi b
-      piArrow b =  SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) b} )
       fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
       fArrowComm1 a b f x OneObj = refl
       fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
@@ -293,116 +287,83 @@
                 ub b (FMap U f x) y
              ≡⟨⟩
                 hom (ob b (FMap U f x)) y
-             ≡⟨⟩
-                ( Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ) y
              ∎ ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-      fArrow :  (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
-      fArrow a b f x = record { arrow = f ; comm = fArrowComm a b f x }
-      preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ]
-         ≈ Sets [ ub a x  o FMap (K Sets A *) (arrow (piArrow (ob a x))) ] ]
-      preinitComm a x = comm (piArrow (ob a x ))
-      equ : {a b : Obj A} → (f g : Hom A a b)  → IsEqualizer A (equalizer-e comp f g ) f g
-      equ f g = Complete.isEqualizer comp f g 
-      ep : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
-      ep {a} {b} {f} {g} = equalizer-p comp f g
-      ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a 
-      ee {a} {b} {f} {g} = equalizer-e comp f g
-      preinitialEqu : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y ) → 
-          IsEqualizer A ee (A [ arrow f o arrow ( preinitialArrow PI {x}) ] ) ( arrow ( preinitialArrow PI {y}) ) 
-      preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (preinitialArrow PI)  ] ) ( arrow ( preinitialArrow PI )) 
-      pa : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y )
-         → Hom ( K (Sets) A * ↓ U) (preinitialObj PI)
-           (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} )
-      pa {x} {y} f = piArrow (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} ) 
-        --
-        --         e             f
-        --    c  -------→ a ---------→ b
-        --    ^        .     ---------→
-        --    |      .            g
-        --    |k   .
-        --    |  . h
-        --    d
-        --
-      comm13 : (a b : Obj ( K Sets A * ↓ U)) (f : Hom ( K Sets A * ↓ U) a b )  → ( K Sets A * ↓ U) [
-           ( K Sets A * ↓ U) [ f o preinitialArrow PI ]  ≈ preinitialArrow PI ]   
-      comm13 a b f = let open ≈-Reasoning A in begin
-                arrow ( ( K Sets A * ↓ U) [ f o preinitialArrow PI ] ) 
-             ≈⟨⟩
-                arrow f o arrow ( preinitialArrow PI {{!!}})
-             ≈⟨ {!!} ⟩
-                arrow ( preinitialArrow PI {{!!}} )
-             ∎  
-      comm12 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( K Sets A * ↓ U) [
-          FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) ≈ FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) ] 
-      comm12 a b f y = let open ≈-Reasoning ( K Sets A * ↓ U) in begin
-                FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) 
-             ≈⟨ {!!} ⟩
-                FMap (SFSF SFS) ( fArrow a b f y ) o FMap (SFSF SFS) ( piArrow (ob a y)) 
-             ≈⟨ {!!} ⟩
-                FMap (SFSF SFS) ( fArrow a b f y ) o preinitialArrow PI {FObj (SFSF SFS) (ob a y ) }
-             ≈⟨ comm13 (FObj (SFSF SFS) (ob a y)) (FObj (SFSF SFS) (ob b (FMap U f y))) (FMap (SFSF SFS) (fArrow a b f y)) ⟩
-                preinitialArrow PI {FObj (SFSF SFS) (ob b (FMap U f y )) }
-             ≈⟨ {!!} ⟩
-                FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) 
-             ∎ 
+      fArrow :  {a b : Obj A} (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
+      fArrow {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
       comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
-         ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
-           ≡ (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
+         ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob a x))) ] ) y   
+           ≡ (Sets [ ( λ x → arrow (initial In (ob b x))) o FMap U f ] ) y
       comm11 a b f y = begin
-               ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
-             ≡⟨⟩
-                 A [ f o arrow (piArrow (ob a y)) ]
-             ≡⟨⟩
-                 A [ arrow ( fArrow a b f y )  o arrow (piArrow (ob a y)) ]
+               ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob a x))) ] ) y   
              ≡⟨⟩
-                arrow ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] )
-             ≡⟨ {!!} ⟩
-                arrow ( ( SFSFMap← SFS ) (  FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] ) ) )
-             ≡⟨ ≡-cong ( λ k → arrow ( (SFSFMap← SFS ) k ))  ( ≈-≡ ( K Sets A * ↓ U) ( comm12 a b f y ) ) ⟩
-                arrow ( ( SFSFMap← SFS ) (  FMap (SFSF SFS) ( piArrow (ob b (FMap U f y) ) )) )
-             ≡⟨ {!!} ⟩
-                arrow (piArrow (ob b (FMap U f y) ))
+                 A [ f o arrow (initial In (ob a y)) ]
              ≡⟨⟩
-                (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
+                 A [ arrow ( fArrow f y ) o arrow (initial In (ob a y)) ]
+             ≡⟨  ≈-≡ A ( uniqueness In {ob b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow f y  o initial In (ob a y)] ) ) ⟩
+                arrow (initial In (ob b (FMap U f y) ))
+             ≡⟨⟩
+                (Sets [ ( λ x → arrow (initial In (ob b x))) o FMap U f ] ) y
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
-      tmap1 b x =  arrow ( piArrow ( ob b x ) )
-      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 ] ]
+      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b)
+      tmap1 b x = arrow ( initial In (ob b x ) ) 
+      comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
       comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
-                FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a 
+                FMap (Yoneda A (obj i)) f o tmap1 a 
              ≈⟨⟩
-                FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow ( ob a x )))  
+                FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob a x )))  
              ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
-                ( λ x → arrow (piArrow (ob b x))) o FMap U f 
+                ( λ x → arrow (initial In (ob b x))) o FMap U f 
              ≈⟨⟩
                 tmap1 b o FMap U f 
              ∎ 
-      comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) → 
-          (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡
-                (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] )  y
+      comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) → 
+          (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡
+                (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → A [ f o x ] ) ] )  y
       comm21 a b f y = begin
-                FMap U f ( FMap U y (hom (preinitialObj PI) OneObj))
-             ≡⟨ ≡-cong ( λ k → k (hom (preinitialObj PI) OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
-                (FMap U (A [ f o y ] ) ) (hom (preinitialObj PI) OneObj) 
+                FMap U f ( FMap U y (hom i OneObj))
+             ≡⟨ ≡-cong ( λ k → k (hom i OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
+                (FMap U (A [ f o y ] ) ) (hom i OneObj) 
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-      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 )
+      tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj i)) b) (FObj U b)
+      tmap2 b x =  ( FMap U x ) ( hom i OneObj )
       comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
-        Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ]
+        Sets [ tmap2 b o FMap (Yoneda A (obj i)) f ] ]
       comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin
                 FMap U f o tmap2 a 
              ≈⟨⟩
-                FMap U f o ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) )
+                FMap U f o ( λ x → ( FMap U x ) ( hom i OneObj ) )
              ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
-                ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o ( λ x → A [ f o x  ]  )
+                ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → A [ f o x  ]  )
+             ≈⟨⟩
+                ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f 
+             ≈⟨⟩
+                tmap2 b o FMap (Yoneda A (obj i)) f 
+             ∎ 
+      iso→  : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ]
+      iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin
+               ( Sets [ tmap1 x o tmap2 x ] ) y
              ≈⟨⟩
-                ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o FMap (Yoneda A (obj (preinitialObj PI))) f 
+                arrow ( initial In (ob x (( FMap U y ) ( hom i OneObj ) ))) 
+             ≈↑⟨  uniqueness In {!!} ⟩
+               arrow (fArrow y {!!} )
+             ≈⟨ {!!} ⟩
+               arrow (fArrow y (hom i OneObj) )
              ≈⟨⟩
-                tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f 
-             ∎ 
+               y
+             ∎  ))
+      iso←  : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ]
+      iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin 
+               ( Sets [ tmap2 x o tmap1 x ] ) y
+             ≡⟨⟩
+               ( FMap U ( arrow ( initial In (ob x y ) ))  ) ( hom i OneObj )
+             ≡⟨ {!!} ⟩
+               y
+             ∎  ) ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning