Unit and Null types. Methods.

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