diff options
| -rw-r--r-- | HoTT_Base.thy | 3 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 7 | ||||
| -rw-r--r-- | Prod.thy | 19 | ||||
| -rw-r--r-- | Sum.thy | 13 | ||||
| -rw-r--r-- | scratch.thy | 50 |
5 files changed, 73 insertions, 19 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 703f1aa..8c45d35 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -54,7 +54,7 @@ and Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans - \<comment> \<open>Lets \<open>standard\<close> automatically solve inequalities.\<close> + \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> text "Universe types:" @@ -64,6 +64,7 @@ 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)" + \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> section \<open>Type families\<close> diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index c314ed4..8a4417d 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -49,14 +49,17 @@ method wellformed uses jdgmt declares wellform = subsection \<open>Derivation search\<close> -text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments. +text "Combine \<open>simple\<close>, \<open>wellformed\<close> and the universe hierarchy rules to search for derivations of judgments. \<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments. Definitions passed as \<open>unfolds\<close> are unfolded throughout." method derive uses lems unfolds = ( unfold unfolds | simple lems: lems | - match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> + match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> | + rule Universe_hierarchy | + (rule Universe_cumulative, simple lems: lems) | + (rule Universe_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>) )+ @@ -69,4 +69,23 @@ abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarro where "A \<rightarrow> B \<equiv> \<Prod>_:A. B" +section \<open>Unit type\<close> + +axiomatization + Unit :: Term ("\<one>") and + pt :: Term ("\<star>") and + indUnit :: "[Typefam, Term, Term] \<Rightarrow> Term" +where + Unit_form: "\<one> : U(0)" +and + Unit_intro: "\<star> : \<one>" +and + Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>; a : \<one>\<rbrakk> \<Longrightarrow> indUnit C c a : C a" +and + Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>\<rbrakk> \<Longrightarrow> indUnit C c \<star> \<equiv> c" + +lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp +lemmas Unit_comps [comp] = Unit_comp + + end
\ No newline at end of file @@ -60,4 +60,17 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" +section \<open>Null type\<close> + +axiomatization + Null :: Term ("\<zero>") and + indNull :: "[Typefam, Term] \<Rightarrow> Term" +where + Null_form: "\<zero> : U(0)" +and + Null_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> indNull C z : C z" + +lemmas Null_rules [intro] = Null_form Null_elim + + end
\ No newline at end of file diff --git a/scratch.thy b/scratch.thy index 3f66083..ae1bdb5 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,10 +3,11 @@ theory scratch begin -term "UN" - (* Typechecking *) -schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" +schematic_goal "\<lbrakk>A : U(i); B : U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" + by derive + +lemma "\<zero> : U(S S S 0)" by derive @@ -24,13 +25,13 @@ have "f`a`b`c \<equiv> d" by (simplify lems: asm) end -lemma "a : A \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" +lemma "\<lbrakk>A : U(i); a : A\<rbrakk> \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" by simplify lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" by simplify -schematic_goal "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x" +schematic_goal "\<lbrakk>a : A; b: A \<longrightarrow> X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x" by rsimplify lemma @@ -38,7 +39,7 @@ lemma shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" by (simplify lems: assms) -lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk> +lemma "\<lbrakk>a : A; b : B a; B: A \<longrightarrow> U(i); \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" by (simplify) @@ -53,7 +54,6 @@ lemma assumes "a : A" "b : B a" - "B: A \<rightarrow> U" "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y" shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" by (simplify lems: assms) @@ -63,19 +63,20 @@ assumes "a : A" "b : B a" "c : C a b" - "B: A \<rightarrow> U" - "\<And>x. x : A\<Longrightarrow> C x: B x \<rightarrow> U" "\<And>x y z. \<lbrakk>x : A; y : B x; z : C x y\<rbrakk> \<Longrightarrow> d x y z : D x y z" shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. \<^bold>\<lambda>z:C x y. d x y z)`a`b`c \<equiv> d a b c" by (simplify lems: assms) +(* Polymorphic identity function *) + +definition Id :: "Numeral \<Rightarrow> Term" where "Id n \<equiv> \<^bold>\<lambda>A:U(n). \<^bold>\<lambda>x:A. x" + +lemma assumes "A : U 0" and "x:A" shows "(Id 0)`A`x \<equiv> x" unfolding Id_def by (simplify lems: assms) -(* HERE IS HOW WE ATTEMPT TO DO PATH INDUCTION --- VERY GOOD CANDIDATE FOR THESIS SECTION *) -schematic_goal "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x" +(* See if we can find path inverse *) +schematic_goal "\<lbrakk>A : U(i); x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x" apply (rule Prod_intro) - apply (rule Equal_form) - apply assumption+ apply (rule Equal_elim) back back @@ -84,9 +85,26 @@ schematic_goal "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x = back back back - back back back back back back - -thm comp + defer + back + back + back + back + back + back + back + back + back + apply (rule Equal_form) + apply assumption+ + defer + defer + apply assumption + defer + defer + apply (rule Equal_intro) + apply assumption+ +oops end
\ No newline at end of file |