aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-07-11 19:37:07 +0200
committerJosh Chen2018-07-11 19:37:07 +0200
commit9723fc3ffc55b22a2a8ec09cbba80f14c40d7991 (patch)
tree57735319777d3a6423a31bd49161bf810f5b9d94
parenta85feff048010fa945c0e498e45aa5626f54f352 (diff)
Universes implemented. Type rules modified accordingly. No more automatic derivation of "A:U" from "a:A".
Diffstat (limited to '')
-rw-r--r--Equal.thy16
-rw-r--r--EqualProps.thy13
-rw-r--r--HoTT_Base.thy35
-rw-r--r--HoTT_Methods.thy11
-rw-r--r--Prod.thy8
-rw-r--r--Proj.thy26
-rw-r--r--Sum.thy24
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