--- a/freyd2.agda	Wed Jul 05 07:53:07 2017 +0900
+++ b/freyd2.agda	Wed Jul 05 09:39:58 2017 +0900
@@ -383,16 +383,22 @@
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
    tmap-η  y = hom (i y) 
 
-   ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
-   ηf a b f  = record { obj = obj (i b) ; hom = B [ tmap-η b o f ] }
+   sobj  : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U 
+   sobj {a} {b} f = record {obj = b; hom =  f } 
+   solution : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f)
+   solution {a} {b} f = initial (In a) (sobj f)
 
-   solution : (a b  : Obj B)  → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (ηf a b f )
-   solution a b f =  initial (In a) (ηf a b f )
+   univ : (a : Obj B) (b : Obj A)  → (f : Hom B a (FObj U b))
+       → B [ B [ FMap U (arrow (solution f)) o tmap-η a ]  ≈ f ]
+   univ = {!!}
+
+   ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
+   ηf a b f  = sobj ( B [ tmap-η b o f ]  )
 
    F : Functor B A
    F = record {
     FObj = λ b →  obj (i b) 
-    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution x y f)
+    ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ]  ))
     ; isFunctor = record {
              identity =  identity1
            ; distr = distr1 
@@ -432,8 +438,7 @@
 
    nat-ε : NTrans A A (F  ○ U) identityFunctor
    nat-ε  = record {
-         TMap = λ x → arrow (initial (In (FObj U x)) (record { obj = x ; hom = id1 B (FObj U x) }))
-         --     why we cannot write this using solution? should be *(id B) 
+         TMap = λ x → arrow ( solution (id1 B (FObj U x)))
          ; isNTrans = record { commute = comm1 } } where
         comm1 : {a b : Obj A} {f : Hom A a b} →
                 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o