Reorganize code

6 files changed, 303 insertions, 257 deletions

diff --git a/Equal.thy b/Equal.thy
new file mode 100644
index 0000000..b9f676f
--- /dev/null
+++ b/Equal.thy
@@ -0,0 +1,81 @@
+theory Equal
+  imports HoTT_Base Prod
+
+begin
+
+subsection \<open>Equality type\<close>
+  
+    axiomatization
+      Equal :: "[Term, Term, Term] \<Rightarrow> Term"
+
+    syntax
+      "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 101] 100)
+      "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
+    translations
+      "a =[A] b" \<rightleftharpoons> "CONST Equal A a b"
+      "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b"
+    
+    axiomatization
+      refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))") and
+      indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term"  ("(indEqual[_])")
+    where
+      Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U"
+      (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *)
+    and
+      Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x"
+    and
+      Equal_elim [elim]:
+        "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term).
+          \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U;
+            f : \<Prod>x:A. 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 [simp]:
+        "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a"
+    
+    lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2]
+    
+    subsubsection \<open>Properties of equality\<close>
+    
+    text "Symmetry/Path inverse"
+    
+    definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
+      where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y"
+    
+    lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp
+    
+    text "Transitivity/Path composition"
+    
+    \<comment> \<open>"Raw" composition function\<close>
+    definition compose' :: "Term \<Rightarrow> Term"  ("(1compose''[_])")
+      where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))"
+    
+    \<comment> \<open>"Natural" composition function\<close>
+    abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
+      where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q"
+    
+    (**** GOOD CANDIDATE FOR AUTOMATION ****)
+    lemma compose_comp:
+      assumes "a : A"
+      shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp
+    
+    text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof.
+    This would likely involve something like:
+      1. Recognizing that there is a function application that can be simplified.
+      2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>.
+      3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>."
+    
+    lemmas Equal_simps [simp] = inv_comp compose_comp
+    
+    subsubsection \<open>Pretty printing\<close>
+    
+    abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_\<^sup>-\<^sup>1[_, _, _])" 500)
+      where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p"
+    
+    abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_ \<bullet>[_, _, _, _]/ _)")
+      where "p \<bullet>[A,x,y,z] q \<equiv> compose[A,x,y,z]`p`q"
+
+end
\ No newline at end of file
diff --git a/HoTT.thy b/HoTT.thy
deleted file mode 100644
index cfb29df..0000000
--- a/HoTT.thy
+++ /dev/null
@@ -1,248 +0,0 @@
-theory HoTT
-  imports Pure
-begin
-
-section \<open>Setup\<close>
-text "For ML files, routines and setup."
-
-section \<open>Basic definitions\<close>
-text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
-We do not implement universes, but simply follow the informal notation in the HoTT book."
-
-typedecl Term
-
-section \<open>Judgments\<close>
-
-consts
-  is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)" [0] 1000)
-  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
-
-section \<open>Definitional equality\<close>
-text "We take the meta-equality \<open>\<equiv>\<close>, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory.
-
-Note that the Pure framework already provides axioms and results for various properties of \<open>\<equiv>\<close>, which we make use of and extend where necessary."
-
-theorem equal_types:
-  assumes "A \<equiv> B" and "A : U"
-  shows "B : U" using assms by simp
-
-theorem equal_type_element:
-  assumes "A \<equiv> B" and "x : A"
-  shows "x : B" using assms by simp
-
-lemmas type_equality [intro, simp] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated]
-
-section \<open>Type families\<close>
-text "Type families are implemented using meta-level lambda expressions \<open>P::Term \<Rightarrow> Term\<close> that further satisfy the following property."
-
-abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
-  where "P: A \<rightarrow> U \<equiv> (\<And>x::Term. x : A \<Longrightarrow> P(x) : U)"
-
-section \<open>Types\<close>
-
-subsection \<open>Dependent function/product\<close>
-
-axiomatization
-  Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
-  lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
-syntax
-  "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"          ("(3\<Prod>_:_./ _)" 30)
-  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<^bold>\<lambda>_:_./ _)" 30)
-  "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"    ("(3PROD _:_./ _)" 30)
-  "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3%%_:_./ _)" 30)
-translations
-  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
-  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
-  "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
-  "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
-  (* The above syntax translations bind the x in the expressions B, b. *)
-
-abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
-  where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
-
-axiomatization
-  appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
-where
-  Prod_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U"
-and
-  Prod_intro [intro]:
-    "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term). (\<And>x::Term. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)"
-and
-  Prod_elim [elim]:
-    "\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term) (a::Term). \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)"
-and
-  Prod_comp [simp]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
-and
-  Prod_uniq [simp]: "\<And>A f::Term. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
-
-lemmas Prod_formation [intro] = Prod_form Prod_form[rotated]
-
-text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
-
-subsection \<open>Dependent pair/sum\<close>
-
-axiomatization
-  Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
-syntax
-  "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<Sum>_:_./ _)" 20)
-  "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3SUM _:_./ _)" 20)
-translations
-  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
-  "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
-
-abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
-  where "A\<times>B \<equiv> \<Sum>_:A. B"
-
-axiomatization
-  pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
-  indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"
-where
-  Sum_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U"
-and
-  Sum_intro [intro]:
-    "\<And>(A::Term) (B::Term \<Rightarrow> Term) (a::Term) (b::Term). \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)"
-and
-  Sum_elim [elim]:
-    "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::Term) (p::Term).
-      \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> indSum(C)`f`p : C(p)"
-and
-  Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \<equiv> f`a`b"
-
-lemmas Sum_formation [intro] = Sum_form Sum_form[rotated]
-
-text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible.
-Hence only the type family \<open>C\<close> is left as a meta-level argument to the inductor indSum."
-
-subsubsection \<open>Projections\<close>
-
-consts
-  fst :: "[Term, 'a] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
-  snd :: "[Term, 'a] \<Rightarrow> Term"  ("(1snd[/_,/ _])")
-overloading
-  fst_dep \<equiv> fst
-  snd_dep \<equiv> snd
-  fst_nondep \<equiv> fst
-  snd_nondep \<equiv> snd
-begin
-definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
-  "fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)"
-
-definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
-  "snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
-
-definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where
-  "fst_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)"
-
-definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
-  "snd_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)"
-end
-
-lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp
-lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
-
-lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
-lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
-
-\<comment> \<open>Simplification rules for projections\<close>
-lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
-
-subsection \<open>Equality type\<close>
-
-axiomatization
-  Equal :: "[Term, Term, Term] \<Rightarrow> Term"
-syntax
-  "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 101] 100)
-  "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =[_]/ _)" [101, 101] 100)
-translations
-  "a =\<^sub>A b" \<rightleftharpoons> "CONST Equal A a b"
-  "a =[A] b" \<rightharpoonup> "CONST Equal A a b"
-
-axiomatization
-  refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))") and
-  indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term"  ("(indEqual[_])")
-where
-  Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U"
-  (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *)
-and
-  Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x"
-and
-  Equal_elim [elim]:
-    "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term).
-      \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U;
-        f : \<Prod>x:A. 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 [simp]:
-    "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a"
-
-lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2]
-
-subsubsection \<open>Properties of equality\<close>
-
-text "Symmetry/Path inverse"
-
-definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
-  where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y"
-
-lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp
-
-text "Transitivity/Path composition"
-
-\<comment> \<open>"Raw" composition function\<close>
-abbreviation compose' :: "Term \<Rightarrow> Term"  ("(1compose''[_])")
-  where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))"
-
-\<comment> \<open>"Natural" composition function\<close>
-abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
-  where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q"
-
-(**** GOOD CANDIDATE FOR AUTOMATION ****)
-lemma compose_comp:
-  assumes "a : A"
-  shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] by simp
-
-text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof.
-This would likely involve something like:
-  1. Recognizing that there is a function application that can be simplified.
-  2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>.
-  3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>."
-
-lemmas Equal_simps [simp] = inv_comp compose_comp
-
-subsubsection \<open>Pretty printing\<close>
-
-abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_\<^sup>-\<^sup>1\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_)" 500)
-  where "p\<^sup>-\<^sup>1\<^sub>A\<^sub>,\<^sub>x\<^sub>,\<^sub>y \<equiv> inv[A,x,y]`p"
-
-abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_ \<bullet>\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_/ _)")
-  where "p \<bullet>\<^sub>A\<^sub>,\<^sub>x\<^sub>,\<^sub>y\<^sub>,\<^sub>z q \<equiv> compose[A,x,y,z]`p`q"
-
-end
-
-(*
-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 *)
-
-*)
\ No newline at end of file
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
new file mode 100644
index 0000000..9650c4c
--- /dev/null
+++ b/HoTT_Base.thy
@@ -0,0 +1,52 @@
+(*  Title:  HoTT/HoTT_Base.thy
+    Author: Josh Chen
+
+Basic setup and definitions of a homotopy type theory object logic.
+*)
+
+theory HoTT_Base
+  imports Pure
+
+begin
+
+section \<open>Basic definitions\<close>
+
+text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
+We do not implement universes, but simply follow the informal notation in the HoTT book."
+
+typedecl Term
+
+section \<open>Judgments\<close>
+
+consts
+is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)" [0] 1000)
+is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
+
+
+section \<open>Definitional equality\<close>
+
+text "We use the Pure equality \<open>\<equiv>\<close> for definitional/judgmental equality of types and terms in our theory."
+
+theorem equal_types:
+  assumes "A \<equiv> B" and "A : U"
+  shows "B : U" using assms by simp
+
+theorem equal_type_element:
+  assumes "A \<equiv> B" and "x : A"
+  shows "x : B" using assms by simp
+
+lemmas type_equality [intro, simp] =
+  equal_types
+  equal_types[rotated]
+  equal_type_element
+  equal_type_element[rotated]
+
+
+section \<open>Type families\<close>
+
+text "A type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property."
+
+abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
+  where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P(x) : U)"
+
+end
\ No newline at end of file
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index f05363a..95f1d0c 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -6,13 +6,13 @@ text "A bunch of theorems and other statements for sanity-checking, as well as t
 
 Things that *should* be automated:
   \<bullet> Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
-  \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
-"
+  \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?"
 
 \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
 declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=1]]
 
-section \<open>Functions\<close>
+
+section \<open>\<Prod> type\<close>
 
 subsection \<open>Typing functions\<close>
 
@@ -35,6 +35,7 @@ proof
   then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. 
 qed
 
+
 subsection \<open>Function application\<close>
 
 proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by simp
@@ -47,7 +48,10 @@ lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f
 
 lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). \<^bold>\<lambda>z:C(x)(y). f x y z)`a`b`c \<equiv> f a b c" by simp
 
-proposition wellformed_currying:
+
+subsection \<open>Currying functions\<close>
+
+proposition curried_function_formation:
   fixes
     A::Term and
     B::"Term \<Rightarrow> Term" and
@@ -67,7 +71,7 @@ proof
 qed (rule assms)
 
 (**** GOOD CANDIDATE FOR AUTOMATION - EISBACH! ****)
-proposition triply_curried:
+proposition higher_order_currying_formation:
   fixes
     A::Term and
     B::"Term \<Rightarrow> Term" and
@@ -94,7 +98,8 @@ proof
   qed
 qed (rule assms)
 
-lemma curried_type:
+(**** AND PROBABLY THIS TOO? ****)
+lemma curried_type_judgment:
   fixes
     a b A::Term and
     B::"Term \<Rightarrow> Term" and
@@ -115,6 +120,9 @@ qed
 text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately!
 This is the result of the choices made regarding the premises of the type rules."
 
+
+section \<open>\<Sum> type\<close>
+
 text "The following shows that the dependent sum inductor has the type we expect it to have:"
 
 lemma
@@ -126,7 +134,7 @@ proof -
     "P \<equiv> \<Sum>x:A. B(x)"
 
   have "\<^bold>\<lambda>f:F. \<^bold>\<lambda>p:P. indSum(C)`f`p : \<Prod>f:F. \<Prod>p:P. C(p)"
-  proof (rule curried_type)
+  proof (rule curried_type_judgment)
     fix f p::Term
     assume "f : F" and "p : P"
     with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def ..
@@ -135,15 +143,42 @@ proof -
   then show "indSum(C) : \<Prod>f:F. \<Prod>p:P. C(p)" by simp
 qed
 
+(**** AUTOMATION CANDIDATE ****)
+text "Propositional uniqueness principle for dependent sums:"
+
+text "We would like to eventually automate proving that 'a given type \<open>A\<close> is inhabited', i.e. search for an element \<open>a:A\<close>.
+
+A good starting point would be to automate the application of elimination rules."
+
+notepad begin
+
+fix A B assume "A : U" and "B: A \<rightarrow> U"
+
+define C where "C \<equiv> \<lambda>p. p =[\<Sum>x:A. B(x)] (fst[A,B]`p, snd[A,B]`p)"
+have *: "C: \<Sum>x:A. B(x) \<rightarrow> U"
+proof -
+  fix p assume "p : \<Sum>x:A. B(x)"
+  have "(fst[A,B]`p, snd[A,B]`p) : \<Sum>x:A. B(x)"
+
+define f where "f \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). refl((x,y))"
+have "f`x`y : C((x,y))"
+sorry
+
+have "p : \<Sum>x:A. B(x) \<Longrightarrow> indSum(C)`f`p : C(p)" using * ** by (rule Sum_elim)
+
+end
+
+section \<open>Universes and polymorphism\<close>
+
 text "Polymorphic identity function."
 
 consts Ui::Term
 
 definition Id where "Id \<equiv> \<^bold>\<lambda>A:Ui. \<^bold>\<lambda>x:A. x"
-(* Have to think about universes... *)
+
 
 (*
-section \<open>Nats\<close>
+section \<open>Natural numbers\<close>
 
 text "Here's a dumb proof that 2 is a natural number."
 
diff --git a/Prod.thy b/Prod.thy
new file mode 100644
index 0000000..9ecab4d
--- /dev/null
+++ b/Prod.thy
@@ -0,0 +1,48 @@
+(*  Title:  HoTT/Prod.thy
+    Author: Josh Chen
+
+Dependent product (function) type for the HoTT logic.
+*)
+
+theory Prod
+  imports HoTT_Base
+
+begin
+
+axiomatization
+  Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
+
+syntax
+  "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"          ("(3\<Prod>_:_./ _)" 30)
+  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<^bold>\<lambda>_:_./ _)" 30)
+  "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"    ("(3PROD _:_./ _)" 30)
+  "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3%%_:_./ _)" 30)
+
+\<comment> \<open>The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>.\<close>
+translations
+  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
+  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
+  "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
+  "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
+
+\<comment> \<open>Type rules\<close>
+axiomatization where
+  Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U"
+and
+  Prod_intro [intro]: "\<And>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 [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)"
+and
+  Prod_comp [simp]: "\<And>A b a. a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
+and
+  Prod_uniq [simp]: "\<And>A f. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+
+text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
+
+\<comment> \<open>Nondependent functions are a special case.\<close>
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
+  where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
+
+end
\ No newline at end of file
diff --git a/Sum.thy b/Sum.thy
new file mode 100644
index 0000000..e34749a
--- /dev/null
+++ b/Sum.thy
@@ -0,0 +1,78 @@
+(*  Title:  HoTT/Sum.thy
+    Author: Josh Chen
+
+Dependent sum type.
+*)
+
+theory Sum
+  imports HoTT_Base Prod
+
+begin
+
+axiomatization
+  Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
+  indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"
+
+syntax
+  "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<Sum>_:_./ _)" 20)
+  "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3SUM _:_./ _)" 20)
+
+translations
+  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
+  "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
+
+axiomatization where
+  Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U"
+and
+  Sum_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)"
+and
+  Sum_elim [elim]: "\<And>A B C f p.
+    \<lbrakk> C: \<Sum>x:A. B(x) \<rightarrow> U;
+      f : \<Prod>x:A. \<Prod>y:B(x). C((x,y));
+      p : \<Sum>x:A. B(x) \<rbrakk> \<Longrightarrow> indSum(C)`f`p : C(p)"
+and
+  Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \<equiv> f`a`b"
+
+text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible.
+Hence only the type family \<open>C\<close> is left as a meta-level argument to the inductor indSum."
+
+\<comment> \<open>Nondependent pair\<close>
+abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
+  where "A\<times>B \<equiv> \<Sum>_:A. B"
+
+subsubsection \<open>Projections\<close>
+
+consts
+  fst :: "[Term, 'a] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
+  snd :: "[Term, 'a] \<Rightarrow> Term"  ("(1snd[/_,/ _])")
+
+overloading
+  fst_dep \<equiv> fst
+  snd_dep \<equiv> snd
+  fst_nondep \<equiv> fst
+  snd_nondep \<equiv> snd
+begin
+  definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
+    "fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)"
+  
+  definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
+    "snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
+  
+  definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where
+    "fst_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)"
+  
+  definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
+    "snd_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)"
+end
+
+text "Simplification rules for the projections:"
+
+lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp
+lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
+
+lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
+lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
+
+lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
+end
\ No newline at end of file