Cleanups and reorganization

10 files changed, 153 insertions, 397 deletions

diff --git a/Coprod.thy b/Coprod.thy
deleted file mode 100644
index b0a1ad2..0000000
--- a/Coprod.thy
+++ /dev/null
@@ -1,50 +0,0 @@
-(*
-Title:  Coprod.thy
-Author: Joshua Chen
-Date:   2018
-
-Coproduct type
-*)
-
-theory Coprod
-imports HoTT_Base
-
-begin
-
-
-axiomatization
-  Coprod    :: "[t, t] \<Rightarrow> t"  (infixr "+" 50) and
-  inl       :: "t \<Rightarrow> t" and
-  inr       :: "t \<Rightarrow> t" and
-  indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>+)")
-where
-  Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and
-
-  Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" and
-
-  Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" and
-
-  Coprod_elim: "\<lbrakk>
-    u: A + B;
-    C: A + B \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> c x: C (inl x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" and
-
-  Coprod_comp_inl: "\<lbrakk>
-    a: A;
-    C: A + B \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> c x: C (inl x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" and
-
-  Coprod_comp_inr: "\<lbrakk>
-    b: B;
-    C: A + B \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> c x: C (inl x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b"
-
-lemmas Coprod_form [form]
-lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim
-lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr
-
-
-end
diff --git a/Empty.thy b/Empty.thy
deleted file mode 100644
index ee11045..0000000
--- a/Empty.thy
+++ /dev/null
@@ -1,27 +0,0 @@
-(*
-Title:  Empty.thy
-Author: Joshua Chen
-Date:   2018
-
-Empty type
-*)
-
-theory Empty
-imports HoTT_Base
-
-begin
-
-
-axiomatization
-  Empty    :: t  ("\<zero>") and
-  indEmpty :: "t \<Rightarrow> t"  ("(1ind\<^sub>\<zero>)")
-where
-  Empty_form: "\<zero>: U O" and
-
-  Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a"
-
-lemmas Empty_form [form]
-lemmas Empty_routine [intro] = Empty_form Empty_elim
-
-
-end
diff --git a/Eq.thy b/Eq.thy
index e93dd8a..7783682 100644
--- a/Eq.thy
+++ b/Eq.thy
@@ -54,6 +54,9 @@ method path_ind for a b p :: t =
 method path_ind' for C :: "[t, t, t] \<Rightarrow> t" =
   (rule Eq_elim[where ?C=C]; (assumption | fact)?)
 
+syntax "_induct_over" :: "[idt, idt, idt, t] \<Rightarrow> [t, t, t] \<Rightarrow> t"  ("(2{_, _, _}/ _)" 0)
+translations "{x, y, p} C" \<rightleftharpoons> "\<lambda>x y p. C"
+
 
 section \<open>Properties of equality\<close>
 
@@ -180,8 +183,12 @@ qed (routine add: assms)
 
 text \<open>
 We use the proof of associativity of path composition to demonstrate the process of deriving proof terms.
-The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the form of the proof term in the first place.
+The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the correct form of the proof term in the first place.
 However, using proof scripts the derivation becomes quite easy; we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover.
+
+The proof is sensitive to the order of the quantifiers in the product.
+In particular, changing the order causes unification to fail in the path inductions.
+It seems to be good practice to order the variables in the order over which we will path-induct.
 \<close>
 
 declare[[pretty_pathcomp=false]]
@@ -193,22 +200,22 @@ schematic_goal pathcomp_assoc:
       pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w]
         pathcomp A x z w (pathcomp A x y z p q) r"
   apply (quantify 3)
-  apply (path_ind'
-    "\<lambda>x y p. \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w).
+  apply (path_ind' "{x, y, p}
+    \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w).
       Eq.pathcomp A x y w p (Eq.pathcomp A y z w q r) =[x =[A] w]
         Eq.pathcomp A x z w (Eq.pathcomp A x y z p q) r")
   apply (quantify 2)
-  apply (path_ind'
-    "\<lambda>xa z q. \<Prod>(w: A). \<Prod>(r: z =[A] w).
+  apply (path_ind' "{xa, z, q}
+    \<Prod>(w: A). \<Prod>(r: z =[A] w).
       Eq.pathcomp A xa xa w (refl xa) (Eq.pathcomp A xa z w q r) =[xa =[A] w]
         Eq.pathcomp A xa z w (Eq.pathcomp A xa xa z (refl xa) q) r")
   apply (quantify 2)
-  apply (path_ind'
-    "\<lambda>xb w r. Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w]
+  apply (path_ind' "{xb, w, r}
+    Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w]
       Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r")
-
-  text \<open>\<close>
-
+  
+  text \<open>And now the rest is routine.\<close>
+  
   apply (derive; (rule assms|assumption)?)
   apply (compute, rule assms, assumption)+
   apply (elim Eq_intro, rule Eq_intro, assumption)
diff --git a/Equal.thy b/Equal.thy
deleted file mode 100644
index 17c1c99..0000000
--- a/Equal.thy
+++ /dev/null
@@ -1,219 +0,0 @@
-(********
-Isabelle/HoTT: Equality
-Feb 2019
-
-********)
-
-theory Equal
-imports Prod HoTT_Methods
-
-begin
-
-
-section \<open>Type definitions\<close>
-
-axiomatization
-  Eq    :: "[t, t, t] \<Rightarrow> t" and
-  refl  :: "t \<Rightarrow> t" and
-  indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t"
-
-syntax
-  "_Eq" :: "[t, t, t] \<Rightarrow> t"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
-translations
-  "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b"
-
-axiomatization where
-  Eq_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and
-
-  Eq_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and
-
-  Eq_elim: "\<lbrakk>
-    p: x =[A] y;
-    a: A;
-    b: A;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a b p : C a b p" and
-
-  Eq_comp: "\<lbrakk>
-    a: A;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a a (refl a) \<equiv> f a"
-
-lemmas Eq_form [form]
-lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim
-lemmas Eq_comp [comp]
-
-
-section \<open>Path induction\<close>
-
-text \<open>We set up rudimentary automation of path induction:\<close>
-
-method path_ind for a b p :: t =
-  (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (fact | assumption)?)
-
-
-section \<open>Properties of equality\<close>
-
-subsection \<open>Symmetry (path inverse)\<close>
-
-definition inv :: "[t, t, t, t] \<Rightarrow> t"
-where "inv A x y p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) x y p"
-
-syntax "_inv" :: "t \<Rightarrow> t"  ("~_" [1000])
-
-text \<open>Pretty-printing switch for path inverse:\<close>
-
-ML \<open>val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\<close>
-
-print_translation \<open>
-let fun inv_tr' ctxt [A, x, y, p] =
-  if Config.get ctxt pretty_inv
-  then Syntax.const @{syntax_const "_inv"} $ p
-  else @{const inv} $ A $ x $ y $ p
-in
-  [(@{const_syntax inv}, inv_tr')]
-end
-\<close>
-
-lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A x y p: y =[A] x"
-unfolding inv_def by derive
-
-lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A a a (refl a) \<equiv> refl a"
-unfolding inv_def by derive
-
-declare
-  inv_type [intro]
-  inv_comp [comp]
-
-subsection \<open>Transitivity (path composition)\<close>
-
-schematic_goal transitivity:
-  assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z"
-proof (path_ind x y p, quantify_all)
-  fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" .
-qed (routine add: assms)
-
-definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t"
-where
-  "pathcomp A x y z p q \<equiv>
-    (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) (\<lambda>x. \<lambda>y: A. id (x =[A] y)) x y p)`z`q"
-
-syntax "_pathcomp" :: "[t, t] \<Rightarrow> t"  (infixl "*" 110)
-
-text \<open>Pretty-printing switch for path composition:\<close>
-
-ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<close>
-
-print_translation \<open>
-let fun pathcomp_tr' ctxt [A, x, y, z, p, q] =
-  if Config.get ctxt pretty_pathcomp
-  then Syntax.const @{syntax_const "_pathcomp"} $ p $ q
-  else @{const pathcomp} $ A $ x $ y $ z $ p $ q
-in
-  [(@{const_syntax pathcomp}, pathcomp_tr')]
-end
-\<close>
-
-lemma pathcomp_type:
-  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z"
-  shows "pathcomp A x y z p q: x =[A] z"
-unfolding pathcomp_def by (routine add: transitivity assms)
-
-lemma pathcomp_cmp:
-  assumes "A: U i" and "a: A"
-  shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
-unfolding pathcomp_def by (derive lems: assms)
-
-lemmas pathcomp_type [intro]
-lemmas pathcomp_comp [comp] = pathcomp_cmp
-
-
-section \<open>Higher groupoid structure of types\<close>
-
-schematic_goal pathcomp_idr:
-  assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p"
-proof (path_ind x y p)
-  show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)"
-  by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal pathcomp_idl:
-  assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p"
-proof (path_ind x y p)
-  show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)"
-  by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal pathcomp_invr:
-  assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)"
-proof (path_ind x y p)
-  show
-    "\<And>x. x: A \<Longrightarrow> refl(refl x):
-      pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)"
-  by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal pathcomp_invl:
-  assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)"
-proof (path_ind x y p)
-  show
-    "\<And>x. x: A \<Longrightarrow> refl(refl x):
-      pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)"
-  by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal inv_involutive:
-  assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "?a: inv A y x (inv A x y p) =[x =[A] y] p"
-proof (path_ind x y p)
-  show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)"
-  by (derive lems: assms)
-qed (routine add: assms)
-
-declare[[pretty_pathcomp=false]]
-
-schematic_goal pathcomp_assoc:
-  assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =[A] y"
-  shows 
-    "?a: \<Prod>q: y =[A] z. \<Prod>r: z =[A] w.
-      pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w]
-        pathcomp A x z w (pathcomp A x y z p q) r"
-proof (path_ind x y p)
-  oops
-  schematic_goal l:
-    assumes "A: U i" "x: A" "z: A" "w: A" "q: x =[A] z"
-    shows
-      "?a: \<Prod>r: z =[A] w. pathcomp A x x w (refl x) (pathcomp A y z w q r) =[x =[A] w]
-        pathcomp A x z w (pathcomp A x x z (refl x) q) r"
-  proof (path_ind x z q)
-    oops
-    schematic_goal l':
-      assumes "A: U i" "x: A" "w: A" "r: x =[A] w"
-      shows
-        "?a: pathcomp A x x w (refl x) (pathcomp A x x w (refl x) r) =[x =[A] w]
-          pathcomp A x x w (pathcomp A x x x (refl x) (refl x)) r"
-    proof (path_ind x w r)
-      show "\<And>x. x: A \<Longrightarrow> refl(refl x):
-        pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x]
-          pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)"
-      by (derive lems: assms)
-    qed (routine add: assms)
-
-(* Possible todo:
-   implement a custom version of schematic_goal/theorem that exports the derived proof term.
-*)
-
-definition l'_prftm :: "[t, t, t, t] \<Rightarrow> t"
-where "l'_prftm A x w r\<equiv>
-  indEq
-    (\<lambda>a b c. pathcomp A a a b (refl a) (pathcomp A a a b (refl a) c) =[a =[A] b]
-      pathcomp A a a b (pathcomp A a a a (refl a) (refl a)) c)
-    (\<lambda>x. refl (refl x)) x w r"
-
-
-end
diff --git a/HoTT.thy b/HoTT.thy
index 6c6ad21..e5db673 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,44 +1,40 @@
-(*
-Title:  HoTT.thy
-Author: Joshua Chen
-Date:   2018
+(********
+Isabelle/HoTT
+Feb 2019
 
-Homotopy type theory
-*)
+An experimental implementation of homotopy type theory.
+
+********)
 
 theory HoTT
 imports
+
 (* Basic theories *)
 HoTT_Base
 HoTT_Methods
 
 (* Types *)
-Coprod
-Empty
-Equal
+Eq
 Nat
 Prod
 Sum
-Unit
+More_Types
 
 (* Derived definitions and properties *)
-Equality
 Projections
 Univalence
 
 begin
 
-
 text \<open>Rule bundles:\<close>
 
 lemmas intros =
-  Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
+  Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Eq_intro Cprd_intro_inl Cprd_intro_inr Unit_intro
 
 lemmas elims =
-  Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
+  Nat_elim Prod_elim Sum_elim Eq_elim Cprd_elim Unit_elim Null_elim
 
 lemmas routines =
-  Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine
-
+  Nat_routine Prod_routine Sum_routine Eq_routine Cprd_routine Unit_routine Null_routine
 
 end
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 099a73e..c9744e9 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -51,7 +51,7 @@ method cumulativity declares form = (
 
 section \<open>Deriving typing judgments\<close>
 
-method routine uses add = (rule add | assumption | rule)+
+method routine uses add = (assumption | rule add | rule)+
 
 text \<open>
 The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}.
@@ -65,7 +65,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute
 It also handles universes using @{method hierarchy} and @{method cumulativity}.
 \<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
+method derive uses lems =
+  (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
 
 section \<open>Additional method combinators\<close>
diff --git a/More_Types.thy b/More_Types.thy
new file mode 100644
index 0000000..9125aca
--- /dev/null
+++ b/More_Types.thy
@@ -0,0 +1,83 @@
+(********
+Isabelle/HoTT: Coproduct, unit, and empty types
+Feb 2019
+
+********)
+
+theory More_Types
+imports HoTT_Base
+
+begin
+
+
+section \<open>Coproduct type\<close>
+
+axiomatization
+  Cprd    :: "[t, t] \<Rightarrow> t"  (infixr "+" 50) and
+  inl     :: "[t, t, t] \<Rightarrow> t" and
+  inr     :: "[t, t, t] \<Rightarrow> t" and
+  indCprd :: "[t \<Rightarrow> t, t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
+where
+  Cprd_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and
+
+  Cprd_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl A B a: A + B" and
+
+  Cprd_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr A B b: A + B" and
+
+  Cprd_elim: "\<lbrakk>
+    u: A + B;
+    C: A + B \<leadsto> U i;
+    \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
+    \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d u: C u" and
+
+  Cprd_cmp_inl: "\<lbrakk>
+    a: A;
+    C: A + B \<leadsto> U i;
+    \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
+    \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inl A B a) \<equiv> c a" and
+
+  Cprd_cmp_inr: "\<lbrakk>
+    b: B;
+    C: A + B \<leadsto> U i;
+    \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
+    \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inr A B b) \<equiv> d b"
+
+lemmas Cprd_form [form]
+lemmas Cprd_routine [intro] = Cprd_form Cprd_intro_inl Cprd_intro_inr Cprd_elim
+lemmas Cprd_comp [comp] = Cprd_cmp_inl Cprd_cmp_inr
+
+
+section \<open>Unit type\<close>
+
+axiomatization
+  Unit    :: t and
+  pt      :: t and
+  indUnit :: "[t \<Rightarrow> t, t, t] \<Rightarrow> t"
+where
+  Unit_form: "Unit: U O" and
+
+  Unit_intro: "pt: Unit" and
+
+  Unit_elim: "\<lbrakk>x: Unit; c: C pt; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c x: C x" and
+
+  Unit_cmp: "\<lbrakk>c: C Unit; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c pt \<equiv> c"
+
+lemmas Unit_form [form]
+lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
+lemmas Unit_cmp [comp]
+
+
+section \<open>Empty type\<close>
+
+axiomatization
+  Null    :: t and
+  indNull :: "[t \<Rightarrow> t, t] \<Rightarrow> t"
+where
+  Null_form: "Null: U O" and
+
+  Null_elim: "\<lbrakk>z: Null; C: Null \<leadsto> U i\<rbrakk> \<Longrightarrow> indNull C z: C z"
+
+lemmas Null_form [form]
+lemmas Null_routine [intro] = Null_form Null_elim
+
+end
diff --git a/Nat.thy b/Nat.thy
index 657e790..61e03e8 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -1,49 +1,46 @@
-(*
-Title:  Nat.thy
-Author: Joshua Chen
-Date:   2018
+(********
+Isabelle/HoTT: Natural numbers
+Feb 2019
 
-Natural numbers
-*)
+********)
 
 theory Nat
 imports HoTT_Base
 
 begin
 
-
 axiomatization
-  Nat    :: t  ("\<nat>") and
+  Nat    :: t and
   zero   :: t  ("0") and
   succ   :: "t \<Rightarrow> t" and
-  indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<nat>)")
+  indNat :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t, t] \<Rightarrow> t"
 where
-  Nat_form: "\<nat>: U O" and
+  Nat_form: "Nat: U O" and
 
-  Nat_intro_0: "0: \<nat>" and
+  Nat_intro_0: "0: Nat" and
 
-  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and
+  Nat_intro_succ: "n: Nat \<Longrightarrow> succ n: Nat" and
 
   Nat_elim: "\<lbrakk>
     a: C 0;
-    n: \<nat>;
-    C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" and
+    n: Nat;
+    C: Nat \<leadsto> U i;
+    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a n: C n" and
 
-  Nat_comp_0: "\<lbrakk>
+  Nat_cmp_0: "\<lbrakk>
     a: C 0;
-    C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and
+    C: Nat \<leadsto> U i;
+    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a 0 \<equiv> a" and
 
-  Nat_comp_succ: "\<lbrakk>
+  Nat_cmp_succ: "\<lbrakk>
     a: C 0;
-    n: \<nat>;
-    C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
+    n: Nat;
+    C: Nat \<leadsto> U i;
+    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n)
+  \<rbrakk> \<Longrightarrow> indNat C f a (succ n) \<equiv> f n (indNat C f a n)"
 
 lemmas Nat_form [form]
 lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
-lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
-
+lemmas Nat_comps [comp] = Nat_cmp_0 Nat_cmp_succ
 
 end
diff --git a/Prod.thy b/Prod.thy
index ff62ee6..059932c 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -70,23 +70,6 @@ lemmas Prod_comp [comp] = Prod_cmp Prod_uniq
 lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq
 
 
-section \<open>Universal quantification\<close>
-
-text \<open>
-It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification.
-
-Method @{theory_text quantify_all} converts the goal
-@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"},
-where @{term B} is not a product, to
-@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}.
-
-Method @{theory_text "quantify k"} does the same, but only for the first k unknowns.
-\<close>
-
-method quantify_all = (rule Prod_intro)+
-method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
-
-
 section \<open>Function composition\<close>
 
 definition compose :: "[t, t, t] \<Rightarrow> t"
@@ -146,4 +129,21 @@ by (derive lems: assms cong)
 
 abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x"
 
+
+section \<open>Universal quantification\<close>
+
+text \<open>
+It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification.
+
+Method @{theory_text quantify_all} converts the goal
+@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"},
+where @{term B} is not a product, to
+@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}.
+
+Method @{theory_text "quantify k"} does the same, but only for the first k unknowns.
+\<close>
+
+method quantify_all = (rule Prod_intro)+
+method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
+
 end
diff --git a/Unit.thy b/Unit.thy
deleted file mode 100644
index 7c221f0..0000000
--- a/Unit.thy
+++ /dev/null
@@ -1,32 +0,0 @@
-(*
-Title:  Unit.thy
-Author: Joshua Chen
-Date:   2018
-
-Unit type
-*)
-
-theory Unit
-imports HoTT_Base
-
-begin
-
-
-axiomatization
-  Unit    :: t  ("\<one>") and
-  pt      :: t  ("\<star>") and
-  indUnit :: "[t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<one>)")
-where
-  Unit_form: "\<one>: U O" and
-
-  Unit_intro: "\<star>: \<one>" and
-
-  Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and
-
-  Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
-
-lemmas Unit_form [form]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-lemmas Unit_comp [comp]
-
-end