--- a/freyd2.agda	Wed Jul 05 09:55:31 2017 +0900
+++ b/freyd2.agda	Wed Jul 05 10:30:17 2017 +0900
@@ -388,6 +388,9 @@
    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)
 
+   η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 ]  )
+
    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 {a} {b} f = let open ≈-Reasoning B in begin
@@ -398,8 +401,17 @@
         f 
       ∎  
 
-   η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 ]  )
+   unique : {a : Obj B} { b : Obj A } → { f : Hom B a (FObj U b) } → { g :  Hom A (obj (i a)) b} →
+      B [ B [ FMap U g o  tmap-η a ]  ≈ f ] → A [ arrow (solution f)  ≈ g ]
+   unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin
+        arrow (solution f) 
+      ≈↑⟨ ≡-≈ ( cong (λ k → arrow (solution k)) ( ≈-≡ B ugη=f )) ⟩
+        arrow (solution (B [ FMap U g o tmap-η a ] )) 
+      ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩
+        g 
+      ∎  where
+         comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ]
+         comm1 = let open ≈-Reasoning B in sym idR
 
    F : Functor B A
    F = record {