Type rules now have \"all\" premises explicitly stated, matching the formulation in the HoTT book.

1 files changed, 29 insertions, 15 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 9650c4c..9b422c4 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,5 +1,6 @@
 (*  Title:  HoTT/HoTT_Base.thy
     Author: Josh Chen
+    Date:   Jun 2018
 
 Basic setup and definitions of a homotopy type theory object logic.
 *)
@@ -9,23 +10,43 @@ theory HoTT_Base
 
 begin
 
-section \<open>Basic definitions\<close>
+section \<open>Setup\<close>
 
-text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
-We do not implement universes, but simply follow the informal notation in the HoTT book."
+text "Set up type checking routines, proof methods etc."
+
+
+section \<open>Metalogical definitions\<close>
+
+text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
+Our implementation does not have universes, and we simply use \<open>a : U\<close> as a convenient shorthand meaning ``\<open>a\<close> is a type''."
 
 typedecl Term
 
+
 section \<open>Judgments\<close>
 
 consts
-is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)" [0] 1000)
-is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
+is_a_type :: "Term \<Rightarrow> prop"           ("(1_ :/ U)" [0] 1000)
+is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
+
+
+section \<open>Type families\<close>
+
+text "A (one-variable) type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property."
+
+type_synonym Typefam = "Term \<Rightarrow> Term"
+
+abbreviation is_type_family :: "[Typefam, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
+  where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P x : U)"
+
+text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial."
 
 
 section \<open>Definitional equality\<close>
 
-text "We use the Pure equality \<open>\<equiv>\<close> for definitional/judgmental equality of types and terms in our theory."
+text "The Pure equality \<open>\<equiv>\<close> is used for definitional aka judgmental equality of types and terms."
+
+\<comment> \<open>Do these ever need to be used?
 
 theorem equal_types:
   assumes "A \<equiv> B" and "A : U"
@@ -35,18 +56,11 @@ theorem equal_type_element:
   assumes "A \<equiv> B" and "x : A"
   shows "x : B" using assms by simp
 
-lemmas type_equality [intro, simp] =
+lemmas type_equality =
   equal_types
   equal_types[rotated]
   equal_type_element
   equal_type_element[rotated]
-
-
-section \<open>Type families\<close>
-
-text "A type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property."
-
-abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
-  where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P(x) : U)"
+\<close>
 
 end
\ No newline at end of file