Universes implemented. Type rules modified accordingly. No more automatic derivation of "A:U" from "a:A".

7 files changed, 63 insertions, 70 deletions

diff --git a/Equal.thy b/Equal.thy
index 18a4207..8c5cf29 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -29,26 +29,26 @@ translations
 section \<open>Type rules\<close>
 
 axiomatization where
-  Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U"
+  Equal_form: "\<And>i A a b. \<lbrakk>A : U(i); a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
 and
-  Equal_form_cond1: "\<And>A a b. a =\<^sub>A b : U \<Longrightarrow> A : U"
+  Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)"
 and
-  Equal_form_cond2: "\<And>A a b. a =\<^sub>A b : U \<Longrightarrow> a : A"
+  Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A"
 and
-  Equal_form_cond3: "\<And>A a b. a =\<^sub>A b : U \<Longrightarrow> b : A"
+  Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A"
 and
   Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a) : a =\<^sub>A a"
 and
-  Equal_elim: "\<And>A C f a b p. \<lbrakk>
-    \<And>x y.\<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<rightarrow> U;
+  Equal_elim: "\<And>i A C f a b p. \<lbrakk>
+    \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i);
     \<And>x. x : A \<Longrightarrow> f x : C x x refl(x);
     a : A;
     b : A;
     p : a =\<^sub>A b
     \<rbrakk> \<Longrightarrow> indEqual[A] C f a b p : C a b p"
 and
-  Equal_comp: "\<And>A C f a. \<lbrakk>
-    \<And>x y.\<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<rightarrow> U;
+  Equal_comp: "\<And>i A C f a. \<lbrakk>
+    \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i);
     \<And>x. x : A \<Longrightarrow> f x : C x x refl(x);
     a : A
     \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a"
diff --git a/EqualProps.thy b/EqualProps.thy
index 43b4eb5..17c7fa6 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -19,14 +19,15 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
   where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) x y p"
 
 
-lemma inv_type: assumes "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
+lemma inv_type:
+  assumes "A : U(i)" and "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
   unfolding inv_def
   by (derive lems: assms)
 
-corollary assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x"
+corollary assumes "x =\<^sub>A y : U(i)" and "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x"
   by (derive lems: inv_type assms)
 
-lemma inv_comp: assumes "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
+lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
   unfolding inv_def by (simplify lems: assms)
 
 
@@ -48,11 +49,13 @@ abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compo
 
 
 lemma compose_type:
-assumes "x : A" and "y : A" and "z : A" shows "compose[A,x,y,z] : x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+  assumes "A : U(i)" and "x : A" and "y : A" and "z : A"
+  shows "compose[A,x,y,z] : x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
   unfolding rcompose_def
   by (derive lems: assms)
 
-lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
+lemma compose_comp:
+  assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
   unfolding rcompose_def
   by (simplify lems: assms)
 
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 610e5d8..703f1aa 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -30,21 +30,12 @@ named_theorems comp
 
 section \<open>Judgments\<close>
 
-text "Formalize the basic judgments.
+text "Formalize the context and typing judgments  \<open>a : A\<close>.
 
-For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
-
-The judgment \<open>is_a_type A\<close> expresses the statement ``A is an inhabitant of some universe type'', i.e. ``A is a type''."
+For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it."
 
 consts
-  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ : _)" [0, 1000] 1000)
-  is_a_type :: "Term \<Rightarrow> prop"           ("(1_ : U)" [0] 1000)
-
-
-text "The following fact is used to make explicit the assumption of well-formed contexts."
-
-axiomatization where
-  inhabited_implies_type [intro, elim, wellform]: "\<And>a A. a : A \<Longrightarrow> A : U"
+  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ : _)" [0, 0] 1000)
 
 
 section \<open>Universes\<close>
@@ -62,31 +53,29 @@ where
 and
   Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n"
 
-\<comment> \<open>This lets \<open>standard\<close> prove ordering statements on Numerals.\<close>
-lemmas Numeral_lt_rules [intro] = Numeral_lt_min Numeral_lt_trans
+lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans
+  \<comment> \<open>Lets \<open>standard\<close> automatically solve inequalities.\<close>
 
 text "Universe types:"
 
 axiomatization
-  U :: "Numeral \<Rightarrow> Term"  ("U_")
+  U :: "Numeral \<Rightarrow> Term"  ("U _")
 where
   Universe_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)"
 and
-  Universe_cumulative: "\<And>a i j. \<lbrakk>a : U(i); i <- j\<rbrakk> \<Longrightarrow> a : U(j)"
-
-lemmas Universe_rules [intro] = Universe_hierarchy Universe_cumulative
+  Universe_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)"
 
 
 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."
+text "We define the following abbreviation constraining the output type of a meta lambda expression when given input of certain type."
 
-type_synonym Typefam = "Term \<Rightarrow> Term"
+abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop"  ("_: _ \<longrightarrow> _")
+  where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x : B)"
 
-abbreviation (input) 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 "The above is used to define type families, which are just constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are elements of some universe type."
 
-\<comment> \<open>There is an obvious generalization to multivariate type families, but implementing such an abbreviation would probably involve writing ML code, and is for the moment not really crucial.\<close>
+type_synonym Typefam = "Term \<Rightarrow> Term"
 
 
 end
\ No newline at end of file
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 9a101e5..c314ed4 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -32,7 +32,7 @@ text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<ope
 
 Can also perform typechecking, and search for elements of a type."
 
-method simple uses lems = (assumption | standard | rule lems)+
+method simple uses lems = (assumption | rule lems | standard)+
 
 
 subsection \<open>Wellformedness checker\<close>
@@ -62,13 +62,12 @@ method derive uses lems unfolds = (
 
 subsection \<open>Simplification\<close>
 
-text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> attempt to solve definitional equations by simplifying lambda applications.
+text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> search for lambda applications to simplify and are suitable for solving definitional equalities, as well as harder proofs where \<open>derive\<close> fails.
 
-\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules.
-In this case use \<open>rsimplify\<close> instead.
+It is however not true that these methods are strictly stronger; if they fail to find a suitable substitution they will fail where \<open>derive\<close> may succeed.
 
-Since these methods use \<open>derive\<close>, it is often (but not always) the case that theorems provable with \<open>derive\<close> are also provable with them.
-(Whether this is the case depends on whether the call to \<open>subst (0) comp\<close> fails.)"
+\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules.
+In this case use \<open>rsimplify\<close> instead."
 
 method rsimplify uses lems = (subst (0) comp, derive lems: lems)+
   \<comment> \<open>\<open>subst\<close> performs an equational rewrite according to some computation rule declared as [comp], after which \<open>derive\<close> attempts to solve any new assumptions that arise.\<close>
diff --git a/Prod.thy b/Prod.thy
index bf4e4e9..445ddd8 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -37,13 +37,13 @@ translations
 section \<open>Type rules\<close>
 
 axiomatization where
-  Prod_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U"
+  Prod_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U(i)"
 and
-  Prod_form_cond1: "\<And>A B. (\<Prod>x:A. B x : U) \<Longrightarrow> A : U"
+  Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> A : U(i)"
 and
-  Prod_form_cond2: "\<And>A B. (\<Prod>x:A. B x : U) \<Longrightarrow> B: A \<rightarrow> U"
+  Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 and
-  Prod_intro: "\<And>A B b. \<lbrakk>A : U; \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
+  Prod_intro: "\<And>i A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
 and
   Prod_elim: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
 and
diff --git a/Proj.thy b/Proj.thy
index 31deaf9..f878469 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -47,12 +47,14 @@ section \<open>Properties\<close>
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
-lemma fst_dep_type: assumes "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A"
+lemma fst_dep_type: assumes "\<Sum>x:A. B x : U(i)" and "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A"
   unfolding fst_dep_def
   by (derive lems: assms)
 
 
-lemma fst_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a"
+lemma fst_dep_comp:
+  assumes "A : U(i)" and "B: A \<longrightarrow> U(i)" and "a : A" and "b : B a"
+  shows "fst[A,B]`(a,b) \<equiv> a"
   unfolding fst_dep_def
   by (simplify lems: assms)
 
@@ -82,7 +84,9 @@ qed
 \<close>
 
 
-lemma snd_dep_type: assumes "p : \<Sum>x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)"
+lemma snd_dep_type:
+  assumes "\<Sum>x:A. B x : U(i)" and "p : \<Sum>x:A. B x"
+  shows "snd[A,B]`p : B (fst[A,B]`p)"
   unfolding fst_dep_def snd_dep_def
   by (simplify lems: assms)
 
@@ -97,7 +101,9 @@ qed (assumption | rule assms)+
 \<close>
 
 
-lemma snd_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \<equiv> b"
+lemma snd_dep_comp:
+  assumes "A : U(i)" and "B: A \<longrightarrow> U(i)" and "a : A" and "b : B a"
+  shows "snd[A,B]`(a,b) \<equiv> b"
   unfolding snd_dep_def fst_dep_def
   by (simplify lems: assms)
 
@@ -126,12 +132,14 @@ qed
 
 text "Nondependent projections:"
 
-lemma fst_nondep_type: assumes "p : A \<times> B" shows "fst[A,B]`p : A"
+lemma fst_nondep_type: assumes "A \<times> B : U(i)" and "p : A \<times> B" shows "fst[A,B]`p : A"
   unfolding fst_nondep_def 
   by (derive lems: assms)
 
 
-lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \<equiv> a"
+lemma fst_nondep_comp:
+  assumes "A : U(i)" and "B : U(i)" and "a : A" and "b : B"
+  shows "fst[A,B]`(a,b) \<equiv> a"
   unfolding fst_nondep_def
   by (simplify lems: assms)
 
@@ -148,7 +156,7 @@ qed
 \<close>
 
 
-lemma snd_nondep_type: assumes "p : A \<times> B" shows "snd[A,B]`p : B"
+lemma snd_nondep_type: assumes "A \<times> B : U(i)" and "p : A \<times> B" shows "snd[A,B]`p : B"
   unfolding snd_nondep_def
   by (derive lems: assms)
 
@@ -163,7 +171,9 @@ qed (rule assms)
 \<close>
 
 
-lemma snd_nondep_comp: assumes "a : A" and "b : B" shows "snd[A,B]`(a,b) \<equiv> b"
+lemma snd_nondep_comp:
+  assumes "A : U(i)" and "B : U(i)" and "a : A" and "b : B"
+  shows "snd[A,B]`(a,b) \<equiv> b"
   unfolding snd_nondep_def
   by (simplify lems: assms)
 
diff --git a/Sum.thy b/Sum.thy
index 46bb022..b608e75 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -30,22 +30,22 @@ translations
 section \<open>Type rules\<close>
 
 axiomatization where
-  Sum_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U"
+  Sum_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U(i)"
 and
-  Sum_form_cond1: "\<And>A B. (\<Sum>x:A. B x : U) \<Longrightarrow> A : U"
+  Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> A : U(i)"
 and
-  Sum_form_cond2: "\<And>A B. (\<Sum>x:A. B x : U) \<Longrightarrow> B: A \<rightarrow> U"
+  Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 and
-  Sum_intro: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
+  Sum_intro: "\<And>i A B a b. \<lbrakk>B: A \<longrightarrow> U(i); a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
 and
-  Sum_elim: "\<And>A B C f p. \<lbrakk>
-    C: \<Sum>x:A. B x \<rightarrow> U;
+  Sum_elim: "\<And>i A B C f p. \<lbrakk>
+    C: \<Sum>x:A. B x \<longrightarrow> U(i);
     \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
     p : \<Sum>x:A. B x
     \<rbrakk> \<Longrightarrow> indSum[A,B] C f p : C p"
 and
-  Sum_comp: "\<And>A B C f a b. \<lbrakk>
-    C: \<Sum>x:A. B x \<rightarrow> U;
+  Sum_comp: "\<And>i A B C f a b. \<lbrakk>
+    C: \<Sum>x:A. B x \<longrightarrow> U(i);
     \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
     a : A;
     b : B a
@@ -59,13 +59,5 @@ text "Nondependent pair."
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
-text "The nondependent pair needs its own separate introduction rule."
-
-lemma Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> B"
-proof
-  fix b B assume "b : B"
-  then show "B : U" ..
-qed
-
 
 end
\ No newline at end of file