diff options
| -rw-r--r-- | Equal.thy | 16 | ||||
| -rw-r--r-- | EqualProps.thy | 13 | ||||
| -rw-r--r-- | HoTT_Base.thy | 35 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 11 | ||||
| -rw-r--r-- | Prod.thy | 8 | ||||
| -rw-r--r-- | Proj.thy | 26 | ||||
| -rw-r--r-- | Sum.thy | 24 |
7 files changed, 63 insertions, 70 deletions
@@ -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> @@ -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 @@ -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) @@ -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 |