From c73a924eb679dea0455414a91dcdeb66b3f827f9 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Jun 2018 13:02:44 +0200
Subject: Dependent sum done, I think.

---
 HoTT_Theorems.thy | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'HoTT_Theorems.thy')

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
-- 
cgit v1.2.3