1 files changed, 48 insertions, 63 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 916f6aa..2ad0ac5 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,97 +1,82 @@
-(*  Title:  HoTT/HoTT_Base.thy
-    Author: Josh Chen
+(*
+Title:  HoTT_Base.thy
+Author: Joshua Chen
+Date:   2018
 
-Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell.
+Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy.
 *)
 
 theory HoTT_Base
-  imports Pure
-begin
-
+imports Pure
 
-section \<open>Foundational definitions\<close>
+begin
 
-text "Meta syntactic type for object-logic types and terms."
 
-typedecl Term
+section \<open>Basic setup\<close>
 
+typedecl t  \<comment> \<open>Type of object types and terms\<close>
+typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
 
-text "
-  Formalize the typing judgment \<open>a: A\<close>.
-  For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
-"
+axiomatization
+  O   :: ord and
+  Suc :: "ord \<Rightarrow> ord" and
+  lt  :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999) and
+  leq :: "[ord, ord] \<Rightarrow> prop"  (infix "\<le>" 999)
+where
+  lt_Suc [intro]: "n < (Suc n)" and
+  lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
+  leq_min [intro]: "O \<le> n"
 
-judgment has_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_:/ _)" [0, 0] 1000)
 
+section \<open>Judgment\<close>
 
-section \<open>Universe hierarchy\<close>
+judgment hastype :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
-text "Finite meta-ordinals to index the universes."
 
-typedecl Ord
+section \<open>Universes\<close>
 
 axiomatization
-  O :: Ord and
-  S :: "Ord \<Rightarrow> Ord"  ("S _" [0] 1000) and
-  lt :: "[Ord, Ord] \<Rightarrow> prop"  (infix "<" 999) and
-  leq :: "[Ord, Ord] \<Rightarrow> prop"  (infix "\<le>" 999)
+  U :: "ord \<Rightarrow> t"
 where
-  lt_min: "\<And>n. O < S n"
-and
-  lt_monotone1: "\<And>n. n < S n"
-and
-  lt_monotone2: "\<And>m n. m < n \<Longrightarrow> S m < S n"
-and
-  leq_min: "\<And>n. O \<le> n"
-and
-  leq_monotone1: "\<And>n. n \<le> S n"
-and
-  leq_monotone2: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n"
-
-lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2
-  \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close>
-
-text "Define the universe types."
+  U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
+  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and
+  U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
-axiomatization
-  U :: "Ord \<Rightarrow> Term"
-where
-  U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U i: U j"
-and
-  U_cumulative: "\<And>A i j. \<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
+text \<open>
+Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
+One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
-text "
-  The rule \<open>U_cumulative\<close> is very unsafe: if used as-is it will usually lead to an infinite rewrite loop!
-  To avoid this, it should be instantiated before being applied.
-"
+@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}.
+\<close>
 
 
 section \<open>Type families\<close>
 
-text "
-  The following abbreviation constrains the output type of a meta lambda expression when given input of certain type.
-"
-
-abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop"  ("(1_: _ \<longrightarrow> _)")
+abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop"  ("(1_:/ _ \<longrightarrow> _)")
   where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)"
 
-text "
-  The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types.
-"
+text \<open>
+The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"}, where @{term "A::t"} and @{term "B::t"} are small types.
+\<close>
 
-type_synonym Typefam = "Term \<Rightarrow> Term"
+type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<close>
 
 
 section \<open>Named theorems\<close>
 
-text "
-  Named theorems to be used by proof methods later (see HoTT_Methods.thy).
-  
-  \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
-"
-
-named_theorems wellform
 named_theorems comp
+named_theorems form
+
+text \<open>
+Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
+
+@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute form} declares type formation rules.
+These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
+\<close>
+
+(* Todo: Set up the Simplifier! *)
 
 
 end