Some comments and reorganization

2 files changed, 42 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
 
diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT book/Ch1.thy
index 84a5cf4..65de875 100644
--- a/ex/HoTT Book/Ch1.thy
+++ b/ex/HoTT book/Ch1.thy
@@ -1,3 +1,10 @@
+(*  Title:  HoTT/ex/HoTT book/Ch1.thy
+    Author: Josh Chen
+    Date:   Aug 2018
+
+A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
+*)
+
 theory Ch1
   imports "../../HoTT"
 begin