aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--HoTT_Test.thy (renamed from HoTT_Theorems.thy)59
1 files changed, 35 insertions, 24 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Test.thy
index 79614d3..4c87e78 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Test.thy
@@ -1,54 +1,65 @@
-theory HoTT_Theorems
+(* Title: HoTT/HoTT_Test.thy
+ Author: Josh Chen
+ Date: Aug 2018
+
+This is an old "test suite" from early implementations of the theory, updated for the most recent version.
+It is not always guaranteed to be up to date.
+*)
+
+theory HoTT_Test
imports HoTT
begin
-text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
-Things that *should* be automated:
- \<bullet> Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
- \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?"
+text "
+ A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
+
+ Things that *should* be automated:
+ - Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
+ - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
+"
-\<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]]
+ \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
-section \<open>\<Prod> type\<close>
+
+section \<open>\<Pi>-type\<close>
subsection \<open>Typing functions\<close>
-text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following."
+text "
+ Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
+"
-proposition assumes "A : U" shows "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" using assms ..
+proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" using assms ..
proposition
- assumes "A : U" and "A \<equiv> B"
- shows "\<^bold>\<lambda>x:A. x : B\<rightarrow>A"
+ assumes "A : U(i)" and "A \<equiv> B"
+ shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
proof -
have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp
- moreover have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" using assms(1) ..
- ultimately show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp
+ moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" using assms(1) ..
+ ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
qed
proposition
- assumes "A : U" and "B : U"
- shows "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
-proof
- fix x
- assume "x : A"
- with assms(2) show "\<^bold>\<lambda>y:B. x : B\<rightarrow>A" ..
-qed (rule assms)
+ assumes "A : U(i)" and "B : U(i)"
+ shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A"
+by (simple lems: assms)
subsection \<open>Function application\<close>
-proposition assumes "a : A" shows "(\<^bold>\<lambda>x:A. x)`a \<equiv> a" using assms by simp
+proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (simple lems: assms)
text "Currying:"
lemma
- assumes "a : A"
- shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y"
+ assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)"
+ shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y"
proof
- show "\<And>x. a : A \<Longrightarrow> x : A \<Longrightarrow> \<^bold>\<lambda>y:B x. y : B x \<rightarrow> B x"
+ show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (simple lems: assms)
+qed fact
lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a`b \<equiv> b" by simp