3 files changed, 135 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..b8021cd
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+*.thy~
diff --git a/HoTT.thy b/HoTT.thy
new file mode 100644
index 0000000..9d63388
--- /dev/null
+++ b/HoTT.thy
@@ -0,0 +1,99 @@
+theory HoTT
+imports Pure
+begin
+
+section \<open>Setup\<close>
+
+(* ML files, routines and setup should probably go here *)
+
+section \<open>Basic definitions\<close>
+
+text \<open>
+A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
+
+For now we do not implement universes, but simply follow the informal notation in the HoTT book.
+\<close>
+(* Actually unsure if a single meta-type suffices... *)
+
+typedecl Term
+
+subsection \<open>Judgements\<close>
+
+consts
+  is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)")  (* Add precedences when I figure them out! *)
+  is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop"  ("(_ : _)")
+
+subsection \<open>Basic axioms\<close>
+
+axiomatization
+where
+  inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" and
+  equal_types: "\<And>A B x. A \<equiv> B \<Longrightarrow> x : A \<Longrightarrow> x : B"
+
+subsection \<open>Basic types\<close>
+
+subsubsection \<open>Nondependent function type\<close>
+(*
+Write this for now to test stuff, later I should make
+this an instance of the dependent function. 
+Same for the nondependent product below.
+*)
+
+axiomatization
+  Function :: "Term \<Rightarrow> Term \<Rightarrow> Term"  (infixr "\<rightarrow>" 10) and
+  lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"    (binder "\<^bold>\<lambda>" 10) and  (* precedence! *)
+  appl :: "Term \<Rightarrow> Term \<Rightarrow> Term"      ("(_`_)")
+where
+  Function_form: "\<And>A B. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<rightarrow>B : U" and
+  Function_intro: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b(x) : B) \<Longrightarrow> \<^bold>\<lambda>x. b(x) : A\<rightarrow>B" and
+  Function_elim: "\<And>A B f a. \<lbrakk>f : A\<rightarrow>B; a : A\<rbrakk> \<Longrightarrow> f`a : B"
+  (* beta and eta reductions should go here *)
+
+subsubsection \<open>Nondependent product type\<close>
+
+axiomatization
+  Product :: "Term \<Rightarrow> Term \<Rightarrow> Term"  ("(_\<times>/ _)") and
+  pair :: "Term \<Rightarrow> Term \<Rightarrow> Term"     ("(_,/ _)") and
+  rec_Product :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"  ("(rec'_Product'(_,_,_,_'))")
+where
+  Product_form: "\<And>A B. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<times>B : U" and
+  Product_intro: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A\<times>B" and
+  Product_elim: "\<And>A B C g. \<lbrakk>A : U; B : U; C : U; g : A\<rightarrow>B\<rightarrow>C\<rbrakk> \<Longrightarrow> rec_Product(A,B,C,g) : (A\<times>B)\<rightarrow>C" and
+  Product_comp: "\<And>A B C g a b. \<lbrakk>C : U; g : A\<rightarrow>B\<rightarrow>C; a : A; b : B\<rbrakk> \<Longrightarrow> rec_Product(A,B,C,g)`(a,b) \<equiv> (g`a)`b"
+
+\<comment> \<open>Projection onto first component\<close>
+definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1'(_,_'))") where
+  "proj1(A,B) \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)"
+
+subsubsection \<open>Empty type\<close>
+
+axiomatization
+  Null :: Term and
+  ind_Null :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(ind'_Null'(_,/ _'))")
+where
+  Null_form: "Null : U" and
+  Null_elim: "\<And>C x a. \<lbrakk>x : Null \<Longrightarrow> C(x) : U; a : Null\<rbrakk> \<Longrightarrow> ind_Null(C(x), a) : C(a)"
+
+subsubsection \<open>Natural numbers\<close>
+
+axiomatization
+  Nat :: Term and
+  zero :: Term ("0") and
+  succ :: "Term \<Rightarrow> Term" and  (* how to enforce \<open>succ : Nat\<rightarrow>Nat\<close>? *)
+  ind_Nat :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"
+where
+  Nat_form: "Nat : U" and
+  Nat_intro1: "0 : Nat" and
+  Nat_intro2: "\<And>n. n : Nat \<Longrightarrow> succ n : Nat"
+  (* computation rules *)
+
+subsubsection \<open>Equality type\<close>
+
+axiomatization
+  Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"  ("(_ =_ _)") and
+  refl :: "Term \<Rightarrow> Term"                   ("(refl'(_'))")
+where
+  Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =A b : U" and
+  Equal_intro: "\<And>A x. x : A \<Longrightarrow> refl x : x =A x"
+
+end
+\ No newline at end of file
diff --git a/test.thy b/test.thy
new file mode 100644
index 0000000..94ba900
--- /dev/null
+++ b/test.thy
@@ -0,0 +1,35 @@
+theory test
+imports HoTT
+begin
+
+lemma "Null : U"
+  by (rule Null_form)
+
+lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A"
+proof -
+  have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
+  thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" by (rule Function_intro)
+qed
+
+lemma "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A"
+proof -
+  have "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. x : B \<rightarrow> A" by (rule Function_intro)
+  thus "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" by (rule Function_intro)
+qed
+
+(* The previous proofs are nice, BUT I want to be able to do something like the following:
+lemma "x : A \<Longrightarrow> \<^bold>\<lambda>x. x : B\<rightarrow>B" <Fail>
+i.e. I want to be able to associate a type to variables, and have the type remembered by any
+binding I define later.
+
+Do I need to give up using the \<open>binder\<close> syntax in order to do this?
+*)
+
+lemma "succ(succ 0) : Nat"
+proof -
+  have "(succ 0) : Nat" by (rule Nat_intro2)
+  from this have "succ(succ 0) : Nat" by (rule Nat_intro2)
+qed
+
+
+end
+\ No newline at end of file