diff options
| author | Josh Chen | 2018-06-05 13:02:44 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-06-05 13:02:44 +0200 |
| commit | c73a924eb679dea0455414a91dcdeb66b3f827f9 (patch) | |
| tree | f35b4b8343c14784b467ed94149afe9f93e3c319 /HoTT_Theorems.thy | |
| parent | c087ad35ac9365cad99b022e138348fb68bc9215 (diff) | |
Dependent sum done, I think.
Diffstat (limited to 'HoTT_Theorems.thy')
| -rw-r--r-- | HoTT_Theorems.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index aeddf9f..a44c8f9 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -41,6 +41,8 @@ proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by text "Currying:" +lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)`a`b \<equiv> b" by simp + lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y)`a \<equiv> \<^bold>\<lambda>y:B(a). f a y" by simp lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). \<^bold>\<lambda>z:C(x)(y). f x y z)`a`b`c \<equiv> f a b c" by simp |