Mercurial > hg > Members > atton > agda > systemF
changeset 15:8c735b9ebf5a
Add lemma for Product
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 08 Apr 2014 17:18:00 +0900 |
| parents | 491a08669724 |
| children | 93705fd8f577 |
| files | systemF.agda |
| diffstat | 1 files changed, 3 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/systemF.agda Tue Apr 08 16:42:52 2014 +0900 +++ b/systemF.agda Tue Apr 08 17:18:00 2014 +0900 @@ -36,6 +36,9 @@ π2 : {l : Level} -> {U : Set l} -> {V : Set l} -> (U × V) -> V π2 {l} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y +lemma-product : {l : Level} {U V : Set l} -> U -> V -> U × V +lemma-product u v = < u , v > + lemma-product-pi1 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u lemma-product-pi1 = refl