aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--HoTT_Base.thy3
-rw-r--r--HoTT_Methods.thy7
-rw-r--r--Prod.thy19
-rw-r--r--Sum.thy13
-rw-r--r--scratch.thy50
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>)
)+
diff --git a/Prod.thy b/Prod.thy
index 445ddd8..fbea4df 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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
diff --git a/Sum.thy b/Sum.thy
index b608e75..99b4df2 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -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