Reorganizing theories

9 files changed, 155 insertions, 219 deletions

diff --git a/Coprod.thy b/Coprod.thy
index 97e0566..d97228e 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -1,65 +1,49 @@
-(*  Title:  HoTT/Coprod.thy
-    Author: Josh Chen
+(*
+Title:  Coprod.thy
+Author: Joshua Chen
+Date:   2018
 
 Coproduct type
 *)
 
 theory Coprod
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and type rules\<close>
 
 axiomatization
-  Coprod :: "[t, t] \<Rightarrow> t"  (infixr "+" 50) and
-  inl :: "t \<Rightarrow> t" and
-  inr :: "t \<Rightarrow> t" and
+  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_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);
-    u: A + B
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u"
-and
+    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda> x. c x) (\<lambda>y. d y) 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);
-    a: A
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a"
-and
+    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (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);
-    b: B
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b"
-
-
-text "Admissible formation inference rules:"
-
-axiomatization where
-  Coprod_wellform1: "A + B: U i \<Longrightarrow> A: U i"
-and
-  Coprod_wellform2: "A + B: U i \<Longrightarrow> B: U i"
-
-
-text "Rule attribute declarations:"
-
-lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr
+    \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b"
 
+lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim
 lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr
-lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2
-lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim
 
 
 end
diff --git a/Empty.thy b/Empty.thy
index 107f2d7..3060867 100644
--- a/Empty.thy
+++ b/Empty.thy
@@ -1,28 +1,24 @@
-(*  Title:  HoTT/Empty.thy
-    Author: Josh Chen
+(*
+Title:  Empty.thy
+Author: Joshua Chen
+Date:   2018
 
 Empty type
 *)
 
 theory Empty
-  imports HoTT_Base
-begin
-
+imports HoTT_Base
 
-section \<open>Constants and type rules\<close>
+begin
 
-section \<open>Empty type\<close>
 
 axiomatization
-  Empty :: t  ("\<zero>") and
+  Empty    :: t  ("\<zero>") and
   indEmpty :: "t \<Rightarrow> t"  ("(1ind\<^sub>\<zero>)")
 where
-  Empty_form: "\<zero>: U O"
-and
-  Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U i; z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> z: C z"
-
+  Empty_form: "\<zero>: U O" and
 
-text "Rule attribute declarations:"
+  Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a"
 
 lemmas Empty_routine [intro] = Empty_form Empty_elim
 
diff --git a/HoTT.thy b/HoTT.thy
index abb1085..3f2d475 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -30,7 +30,7 @@ begin
 lemmas forms =
   Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
 lemmas intros =
-  Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro
+  Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
 lemmas elims =
   Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
 lemmas routines =
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 07fbfc4..efc6182 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,7 +1,9 @@
-(*  Title:  HoTT/HoTT_Base.thy
-    Author: Joshua Chen
+(*
+Title:  HoTT_Base.thy
+Author: Joshua Chen
+Date:   2018
 
-Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy.
+Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy.
 *)
 
 theory HoTT_Base
@@ -49,8 +51,8 @@ Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blind
 One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 \<close>
 
-method cumulativity = (elim U_cumulative, proveSuc)  \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>.\<close>
-method hierarchy = (rule U_hierarchy, proveSuc)  \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...)).\<close>\<close>
+method cumulativity = (elim U_cumulative, proveSuc)  \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>\<close>
+method hierarchy = (rule U_hierarchy, proveSuc)  \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...))\<close>\<close>
 
 
 section \<open>Type families\<close>
@@ -59,22 +61,23 @@ abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> pro
   where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)"
 
 text \<open>
-The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"} where @{term "A::t"} and @{term "B::t"} are small types.
+The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"}, where @{term "A::t"} and @{term "B::t"} are small types.
 \<close>
 
-type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families.\<close>
+type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<close>
 
 
 section \<open>Named theorems\<close>
 
+named_theorems comp
+
 text \<open>
 Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
-\<open>wellform\<close> declares necessary well-formedness conditions for type and inhabitation judgments.
-\<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+@{attribute comp} declares computation rules.
+These are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
 \<close>
 
-named_theorems wellform
-named_theorems comp
+(* Todo: Set up the simplifier! *)
 
 
 end
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index abb6dda..9849195 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -1,63 +1,51 @@
-(*  Title:  HoTT/HoTT_Methods.thy
-    Author: Josh Chen
+(*
+Title:  HoTT_Methods.thy
+Author: Joshua Chen
+Date:   2018
 
-Method setup for the HoTT library. Relies heavily on Eisbach.
+Method setup for the HoTT logic. Relies heavily on Eisbach.
 *)
 
 theory HoTT_Methods
-  imports
-    "HOL-Eisbach.Eisbach"
-    "HOL-Eisbach.Eisbach_Tools"
-    HoTT_Base
+imports
+  "HOL-Eisbach.Eisbach"
+  "HOL-Eisbach.Eisbach_Tools"
+  HoTT_Base
+
 begin
 
 
 section \<open>Deriving typing judgments\<close>
 
-method routine uses lems = (assumption | rule lems | standard)+
-
-text "
-  @{method routine} proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas.
-"
-
-text "
-  \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>.
-  If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>.
-  \<open>wellform\<close> is like \<open>wellformed'\<close> but takes multiple judgments.
-
-  The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy.
-"
+method routine uses add = (assumption | rule add | rule)+
 
-method wellformed' uses jdmt declares wellform =
-  match wellform in rl: "PROP ?P" \<Rightarrow> \<open>(
-    catch \<open>rule rl[OF jdmt]\<close> \<open>fail\<close> |
-    catch \<open>wellformed' jdmt: rl[OF jdmt]\<close> \<open>fail\<close>
-    )\<close>
-
-method wellformed uses lems =
-  match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close>
+text \<open>
+The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier \<open>add\<close>.
+\<close>
 
 
 section \<open>Substitution and simplification\<close>
 
-text "Import the \<open>subst\<close> method, used for substituting definitional equalities."
-
 ML_file "~~/src/Tools/misc_legacy.ML"
 ML_file "~~/src/Tools/IsaPlanner/isand.ML"
 ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
 ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
 ML_file "~~/src/Tools/eqsubst.ML"
 
-text "Perform basic single-step computations:"
+\<comment> \<open>Import the @{method subst} method, used for substituting definitional equalities.\<close>
 
-method compute uses lems = (subst lems comp | rule lems comp)
+method compute declares comp = (subst comp)
 
+text \<open>
+Method @{method compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context.
+Premises of the rule(s) applied are added as new subgoals.
+\<close>
 
 section \<open>Derivation search\<close>
 
-text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments."
+text \<open>Combine @{method routine} and @{method compute} to search for derivations of judgments.\<close>
 
-method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+
+method derive uses lems = (routine add: lems | compute comp: lems)+
 
 
 section \<open>Induction\<close>
diff --git a/Nat.thy b/Nat.thy
index a82e7cb..46b1af5 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -1,54 +1,48 @@
-(*  Title:  HoTT/Nat.thy
-    Author: Josh Chen
+(*
+Title:  Nat.thy
+Author: Joshua Chen
+Date:   2018
 
 Natural numbers
 *)
 
 theory Nat
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and type rules\<close>
 
 axiomatization
-  Nat :: t   ("\<nat>") and
-  zero :: t  ("0") and
-  succ :: "t \<Rightarrow> t" and
+  Nat    :: t  ("\<nat>") and
+  zero   :: t  ("0") and
+  succ   :: "t \<Rightarrow> t" and
   indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<nat>)")
 where
-  Nat_form: "\<nat>: U O"
-and
-  Nat_intro_0: "0: \<nat>"
-and
-  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>"
-and
+  Nat_form: "\<nat>: U O" and
+
+  Nat_intro_0: "0: \<nat>" and
+
+  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and
+
   Nat_elim: "\<lbrakk>
-    C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n);
     a: C 0;
-    n: \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n"
-and
+    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> (\<lambda>n c. f n c) a n: C n" and
+
   Nat_comp_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);
-    a: C 0
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a"
-and
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a 0 \<equiv> a" and
+
   Nat_comp_succ: "\<lbrakk>
-    C: \<nat> \<longrightarrow> U i;
-    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n);
     a: C 0;
-    n: \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
-
-
-text "Rule attribute declarations:"
+    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> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
-lemmas Nat_intro = Nat_intro_0 Nat_intro_succ
-lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ
-lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim
+lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
+lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
 
 
 end
diff --git a/Proj.thy b/Proj.thy
index 74c561c..f272224 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -1,62 +1,46 @@
-(*  Title:  HoTT/Proj.thy
-    Author: Josh Chen
+(*
+Title:  Proj.thy
+Author: Joshua Chen
+Date:   2018
 
 Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type.
 *)
 
 theory Proj
-  imports
-    HoTT_Methods
-    Prod
-    Sum
-begin
+imports
+  HoTT_Methods
+  Prod
+  Sum
 
+begin
 
-definition fst :: "Term \<Rightarrow> Term" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
-definition snd :: "Term \<Rightarrow> Term" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
 
-text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
+definition fst :: "t \<Rightarrow> t" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
+definition snd :: "t \<Rightarrow> t" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
 
 lemma fst_type:
-  assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "fst p: A"
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst p: A"
 unfolding fst_def by (derive lems: assms)
 
 lemma fst_comp:
   assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a"
-unfolding fst_def
-proof compute
-  show "a: A" and "b: B a" by fact+
-qed (routine lems: assms)+
+unfolding fst_def by compute (derive lems: assms)
 
 lemma snd_type:
-  assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)"
-unfolding snd_def
-proof
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)"
+unfolding snd_def proof
   show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> B (fst p): U i" by (derive lems: assms fst_type)
   
-  fix x y
-  assume asm: "x: A" "y: B x"
-  show "y: B (fst <x,y>)"
-  proof (subst fst_comp)
-    show "A: U i" by (wellformed lems: assms(1))
-    show "\<And>x. x: A \<Longrightarrow> B x: U i" by (wellformed lems: assms(1))
-  qed fact+
+  fix x y assume asm: "x: A" "y: B x"
+  show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp)
 qed fact
 
 lemma snd_comp:
   assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b"
-unfolding snd_def
-proof compute
-  show "\<And>x y. y: B x \<Longrightarrow> y: B x" .
-  show "a: A" by fact
-  show "b: B a" by fact
-qed (routine lems: assms)
-
-
-text "Rule attribute declarations:"
+unfolding snd_def by (derive lems: assms)
 
-lemmas Proj_type [intro] = fst_type snd_type
-lemmas Proj_comp [comp] = fst_comp snd_comp
+lemmas Proj_types [intro] = fst_type snd_type
+lemmas Proj_comps [comp] = fst_comp snd_comp
 
 
 end
diff --git a/Sum.thy b/Sum.thy
index 92375b9..422e01b 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -1,69 +1,58 @@
-(*  Title:  HoTT/Sum.thy
-    Author: Josh Chen
+(*
+Title:  Sum.thy
+Author: Joshua Chen
+Date:   2018
 
 Dependent sum type
 *)
 
 theory Sum
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and syntax\<close>
 
 axiomatization
-  Sum :: "[t, Typefam] \<Rightarrow> t" and
-  pair :: "[t, t] \<Rightarrow> t"  ("(1<_,/ _>)") and
+  Sum    :: "[t, tf] \<Rightarrow> t" and
+  pair   :: "[t, t] \<Rightarrow> t"  ("(1<_,/ _>)") and
   indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<Sum>)")
 
 syntax
-  "_SUM" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Sum>_:_./ _)" 20)
-  "_SUM_ASCII" :: "[idt, t, t] \<Rightarrow> t"  ("(3SUM _:_./ _)" 20)
+  "_sum" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Sum>_:_./ _)" 20)
+  "_sum_ascii" :: "[idt, t, t] \<Rightarrow> t"  ("(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)"
 
-text "Nondependent pair."
-
 abbreviation Pair :: "[t, t] \<Rightarrow> t"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
+axiomatization where
+\<comment> \<open>Type rules\<close>
 
-section \<open>Type rules\<close>
+  Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" and
+
+  Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" and
 
-axiomatization where
-  Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i"
-and
-  Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x"
-and
   Sum_elim: "\<lbrakk>
     p: \<Sum>x:A. B x;
-    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y>;
-    C: \<Sum>x:A. B x \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p"  (* What does writing \<lambda>x y. f(x, y) change? *)
-and
+    C: \<Sum>x:A. B x \<longrightarrow> U i;
+    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) p: C p" and
+
   Sum_comp: "\<lbrakk>
     a: A;
     b: B a;
-    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y>;
     B: A \<longrightarrow> U i;
-    C: \<Sum>x:A. B x \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b"
-
-text "Admissible inference rules for sum formation:"
-
-axiomatization where
-  Sum_wellform1: "(\<Sum>x:A. B x: U i) \<Longrightarrow> A: U i"
-and
-  Sum_wellform2: "(\<Sum>x:A. B x: U i) \<Longrightarrow> B: A \<longrightarrow> U i"
+    C: \<Sum>x:A. B x \<longrightarrow> U i;
+    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) <a,b> \<equiv> f a b" and
 
+\<comment> \<open>Congruence rules\<close>
 
-text "Rule attribute declarations:"
+  Sum_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x \<equiv> \<Sum>x:A. C x"
 
-lemmas Sum_comp [comp]
-lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2
 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim
+lemmas Sum_comp [comp]
 
 
 end
diff --git a/Unit.thy b/Unit.thy
index 6760f27..61c6439 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -1,33 +1,31 @@
-(*  Title:  HoTT/Unit.thy
-    Author: Josh Chen
+(*
+Title:  Unit.thy
+Author: Joshua Chen
+Date:   2018
 
 Unit type
 *)
 
 theory Unit
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and type rules\<close>
 
 axiomatization
-  Unit :: Term  ("\<one>") and
-  pt :: Term    ("\<star>") and
-  indUnit :: "[Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<one>)")
+  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>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a"
-and
-  Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
+  Unit_form: "\<one>: U O" and
 
+  Unit_intro: "\<star>: \<one>" and
 
-text "Rule attribute declarations:"
+  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_comp [comp]
 lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
+lemmas Unit_comp [comp]
 
 end