Mercurial > hg > Members > kono > Proof > category

changeset 372:b4855a3ebd34

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add more lemma in limit-to
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Mar 2016 02:05:50 +0900
parents 3a125d05ae0f
children 4164586ffdb8
files limit-to.agda
diffstat 1 files changed, 7 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!} 
 
+