--- a/limit-to.agda	Sat Mar 26 15:09:19 2016 +0900
+++ b/limit-to.agda	Sat Mar 26 15:47:46 2016 +0900
@@ -546,13 +546,44 @@
                 commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh 
             }
           }
+         eqlim = lim Γ  {c} {nat1 c e fe=ge }
          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
-         k {d} h fh=gh  = limit (lim Γ  {c} {nat1 c e fe=ge }) d (nat1 d h fh=gh ) 
+         k {d} h fh=gh  = limit eqlim d (nat1 d h fh=gh ) 
          ek=h :  (d : Obj A ) (h : Hom A d a ) ->  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  -> A [ A [ e o k h fh=gh ] ≈ h ]
-         ek=h d h fh=gh = {!!}
+         ek=h d h fh=gh =   begin
+                    e o k h fh=gh
+                ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0}  ⟩
+                    h
+                ∎
+         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) -> A [ A [ e o k' ] ≈ h ] -> A [ A [ nmap i c e o k' ] ≈ nmap i d h ]
+         uniq-nat {t0} d h k' ek'=h =  begin
+                    nmap t0 c e o k'
+                ≈⟨⟩
+                    e o k'
+                ≈⟨ ek'=h ⟩
+                    h
+                ≈⟨⟩
+                    nmap t0 d h
+                ∎
+         uniq-nat {t1} d h k' ek'=h =  begin
+                    nmap t1 c e o k'
+                ≈⟨⟩
+                   (f o e ) o k'
+                ≈↑⟨ assoc ⟩
+                   f o ( e o k' )
+                ≈⟨ cdr  ek'=h ⟩
+                    f o h
+                ≈⟨⟩
+                    nmap t1 d h
+                ∎
          uniquness :  (d : Obj A ) (h : Hom A d a ) ->  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  ->
                  ( k' : Hom A d c )
                 -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
-         uniquness d h fh=gh = {!!}
+         uniquness d h fh=gh k' ek'=h =   begin
+                    k h fh=gh
+                ≈⟨ limit-uniqueness eqlim {d} {nat1 d h fh=gh } {k'} ( \{i} -> uniq-nat {i} d h k' ek'=h ) ⟩
+                    k'
+                ∎
 
 
+