# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1457197550 -32400
# Node ID b4855a3ebd34d05b270397c511a7acf7fabf1c51
# Parent  3a125d05ae0f42cc7625c33945d2cfba5dd26af0
add more lemma in limit-to

diff -r 3a125d05ae0f -r b4855a3ebd34 limit-to.agda
--- a/limit-to.agda	Sun Mar 06 01:56:32 2016 +0900
+++ b/limit-to.agda	Sun Mar 06 02:05:50 2016 +0900
@@ -133,4 +133,11 @@
           }
          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 A Γ  {c} {nat c e fe=ge }) d (nat 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 = {!!} 
+         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 = {!!} 
 
+