From 746fab6476dc622a982d5ebaeb30a2e1426c3316 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 19 Aug 2018 17:28:48 +0200
Subject: Higher groupoid structure of types

---
 EqualProps.thy | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 67 insertions(+), 4 deletions(-)

diff --git a/EqualProps.thy b/EqualProps.thy
index a1d4c45..be8e53e 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -33,7 +33,7 @@ text "
 "
 
 lemma inv_comp:
-  assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
+  assumes "A : U(i)" and "a : A" shows "(refl(a))\<inverse> \<equiv> refl(a)"
 unfolding inv_def
 proof compute
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
@@ -194,7 +194,7 @@ qed fact
 
 text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead."
 
-axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 60) where
+axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 120) where
   pathcomp_def: "\<lbrakk>
     A: U(i);
     x: A; y: A; z: A;
@@ -214,8 +214,71 @@ lemma pathcomp_comp:
 by (subst pathcomp_def) (routine lems: assms rpathcomp_comp)
 
 
-lemmas EqualProps_type [intro] = inv_type pathcomp_type
-lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp
+lemmas inv_type [intro]
+lemmas pathcomp_type [intro]
 
+lemmas inv_comp [comp]
+lemmas pathcomp_comp [comp]
+
+
+section \<open>Weak higher groupoid structure of types\<close>
+
+schematic_goal whg1a:
+  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  shows "?a: p =[x =\<^sub>A y] (p \<bullet> (refl(y)))"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
+  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))"
+  by compute (routine lems: assms)
+qed (routine lems: assms)
+
+schematic_goal whg1b:
+  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  shows "?a: p =[x =\<^sub>A y] (refl(x) \<bullet> p)"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
+  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))"
+  by compute (routine lems: assms)
+qed (routine lems: assms)
+
+schematic_goal whg2a:
+  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
+  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): ((refl(x))\<inverse> \<bullet> refl(x)) =[x =\<^sub>A x] refl(x)"
+  by (compute | routine lems: assms)+
+qed (routine lems: assms)+
+
+schematic_goal whg2b:
+  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
+  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x) \<bullet> (refl(x))\<inverse>) =[x =\<^sub>A x] refl(x)"
+  by (compute | routine lems: assms)+
+qed (routine lems: assms)+
+
+schematic_goal whg3:
+  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
+  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x))\<inverse>\<inverse> =[x =\<^sub>A x] refl(x)"
+  by (compute | routine lems: assms)+
+qed (routine lems: assms)
+
+
+lemma assumes "A: U(i)" shows "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x"
+by (rule Prod_atomize[where ?A=A and ?B="\<lambda>x. x =\<^sub>A x"]) (routine lems: assms)
+
+
+schematic_goal
+  assumes
+    "A: U(i)" and
+    "x: A" "y: A" "z: A" "w: A" and
+    "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
+  shows
+    "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
+  fix y assume "y: A"
+  show "refl(q \<bullet> r): refl(y) \<bullet> (q \<bullet> r) =[y =\<^sub>A w] (refl(y) \<bullet> q) \<bullet> r"
+  proof (compute lems: whg1b)
+  
 
 end
-- 
cgit v1.2.3


From ae909b21905be847a2ce01388e34708c9d0246c0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 19 Aug 2018 17:29:25 +0200
Subject: Trying to atomize universal quantification

---
 Prod.thy | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Prod.thy b/Prod.thy
index b0408b9..3b74531 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -81,4 +81,13 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 70)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
 
+section \<open>Atomization\<close>
+
+text "
+  Universal statements can be internalized within the theory; the following rule is admissible.
+" (* PROOF NEEDED *)
+
+axiomatization where Prod_atomize: "(\<^bold>\<lambda>x. b(x): \<Prod>x:A. B(x)) \<Longrightarrow> (\<And>x. x: A \<Longrightarrow> b(x): B(x))"
+
+
 end
-- 
cgit v1.2.3


From 515872533295e8464799467303fff923b52a2c01 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 15 Sep 2018 20:51:39 +0200
Subject: begin reorganizing

---
 HoTT_Base.thy  | 19 ++++++++++---------
 tests/Test.thy |  2 +-
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 1110e14..8ea767f 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,11 +1,12 @@
 (*  Title:  HoTT/HoTT_Base.thy
-    Author: Josh Chen
+    Author: Joshua Chen
 
 Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell.
 *)
 
 theory HoTT_Base
-  imports Pure
+imports Pure
+
 begin
 
 
@@ -13,7 +14,7 @@ section \<open>Foundational definitions\<close>
 
 text "Meta syntactic type for object-logic types and terms."
 
-typedecl Term
+typedecl t
 
 
 section \<open>Judgments\<close>
@@ -23,19 +24,19 @@ text "
   For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
 "
 
-judgment has_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_:/ _)" [0, 0] 1000)
+judgment hastype :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
 
 section \<open>Universe hierarchy\<close>
 
-text "Finite meta-ordinals to index the universes."
+text "Meta-numerals to index the universes."
 
-typedecl Ord
+typedecl ord
 
 axiomatization
-  O :: Ord and
-  S :: "Ord \<Rightarrow> Ord"  ("S_" [0] 1000) and
-  lt :: "[Ord, Ord] \<Rightarrow> prop"  (infix "<-" 999)
+  O :: ord and
+  S :: "ord \<Rightarrow> ord"  ("S_") and
+  lt :: "[ord, ord] \<Rightarrow> prop"  (infix "<-" 999)
 where
   Ord_min: "\<And>n. O <- S(n)"
 and
diff --git a/tests/Test.thy b/tests/Test.thy
index b0eb87a..de65dbd 100644
--- a/tests/Test.thy
+++ b/tests/Test.thy
@@ -23,7 +23,7 @@ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit
   \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
 
 
-section \<open>\<Pi>-type\<close>
+section \<open>\<Prod>-type\<close>
 
 subsection \<open>Typing functions\<close>
 
-- 
cgit v1.2.3


From ea0c0c5427888982adce10ab25cebe445997f08b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 13:13:08 +0200
Subject: Moved function composition lemmas into Prod.thy

---
 Prod.thy      | 102 +++++++++++++++++++++++++++++-----------------------------
 ProdProps.thy |  57 --------------------------------
 2 files changed, 51 insertions(+), 108 deletions(-)
 delete mode 100644 ProdProps.thy

diff --git a/Prod.thy b/Prod.thy
index a3cc347..db18454 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -1,89 +1,89 @@
-(*  Title:  HoTT/Prod.thy
-    Author: Josh Chen
+(*
+Title:  Prod.thy
+Author: Joshua Chen
+Date:   2018
 
-Dependent product (function) type
+Dependent product type
 *)
 
 theory Prod
-  imports HoTT_Base
+imports HoTT_Base HoTT_Methods
+
 begin
 
 
-section \<open>Constants and syntax\<close>
+section \<open>Basic definitions\<close>
 
 axiomatization
-  Prod :: "[t, tf] \<Rightarrow> t" and
+  Prod   :: "[t, tf] \<Rightarrow> t" and
   lambda :: "(t \<Rightarrow> t) \<Rightarrow> t"  (binder "\<^bold>\<lambda>" 30) and
-  appl :: "[t, t] \<Rightarrow> t"  (infixl "`" 60)
-    \<comment> \<open>Application binds tighter than abstraction.\<close>
+  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`/_)" [60, 61] 60)  \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
-  "_PROD" :: "[idt, t, t] \<Rightarrow> t"          ("(3\<Prod>_:_./ _)" 30)
-  "_PROD_ASCII" :: "[idt, t, t] \<Rightarrow> t"    ("(3PROD _:_./ _)" 30)
+  "_prod" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Prod>_:_./ _)" 30)
+  "_prod_ascii" :: "[idt, t, t] \<Rightarrow> t"  ("(3II _:_./ _)" 30)
 
-text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>."
+text \<open>The translations below bind the variable @{term x} in the expressions @{term B} and @{term b}.\<close>
 
 translations
   "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
-  "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
+  "II x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
 
-text "Nondependent functions are a special case."
+text \<open>Non-dependent functions are a special case.\<close>
 
-abbreviation Function :: "[t, t] \<Rightarrow> t"  (infixr "\<rightarrow>" 40)
+abbreviation Fun :: "[t, t] \<Rightarrow> t"  (infixr "\<rightarrow>" 40)
   where "A \<rightarrow> B \<equiv> \<Prod>_: A. B"
 
+axiomatization where
+\<comment> \<open>Type rules\<close>
 
-section \<open>Type rules\<close>
+  Prod_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x: U i" and
 
-axiomatization where
-  Prod_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x: U i"
-and
-  Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x: \<Prod>x:A. B x"
-and
-  Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a"
-and
-  Prod_appl: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a"
-and
-  Prod_uniq: "f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f"
-and
-  Prod_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x \<equiv> \<^bold>\<lambda>x. c x"
-
-text "
-  The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule.
-
-  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).
-"
-
-text "
-  In addition to the usual type rules, it is a meta-theorem that whenever \<open>\<Prod>x:A. B x: U i\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U i\<close> and \<open>B: A \<longrightarrow> U i\<close>.
-  
-  That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly.
-"
+  Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x: \<Prod>x:A. B x" and
 
-axiomatization where
-  Prod_wellform1: "(\<Prod>x:A. B x: U i) \<Longrightarrow> A: U i"
-and
-  Prod_wellform2: "(\<Prod>x:A. B x: U i) \<Longrightarrow> B: A \<longrightarrow> U i"
+  Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and
+
+  Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and
+
+  Prod_uniq: "f: \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. f`x \<equiv> f" and
 
+\<comment> \<open>Congruence rules\<close>
 
-text "Rule attribute declarations---set up various methods to use the type rules."
+  Prod_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> \<Prod>x:A. B x \<equiv> \<Prod>x:A. C x" and
+
+  Prod_intro_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x \<equiv> \<^bold>\<lambda>x. c x"
+
+text \<open>
+The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions.
+The actual definitional equality rule is @{thm Prod_intro_eq}.
+Note that this is a separate rule from function extensionality.
+
+Note that the bold lambda symbol \<open>\<^bold>\<lambda>\<close> used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation).
+\<close>
 
-lemmas Prod_comp [comp] = Prod_appl Prod_uniq
-lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2
 lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
+lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
 
-section \<open>Function composition\<close>
+section \<open>Additional definitions\<close>
 
 definition compose :: "[t, t] \<Rightarrow> t"  (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)"
-
-syntax "_COMPOSE" :: "[t, t] \<Rightarrow> t"  (infixr "\<circ>" 110)
+syntax "_compose" :: "[t, t] \<Rightarrow> t"  (infixr "\<circ>" 110)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
+declare compose_def [comp]
+
+lemma compose_assoc:
+  assumes "A: U i" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D x"
+  shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)"
+by (derive lems: assms Prod_intro_eq)
 
-section \<open>Polymorphic identity function\<close>
+lemma compose_comp:
+  assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x"
+  shows "(\<^bold>\<lambda>x. c x) \<circ> (\<^bold>\<lambda>x. b x) \<equiv> \<^bold>\<lambda>x. c (b x)"
+by (derive lems: assms Prod_intro_eq)
 
-abbreviation id :: t where "id \<equiv> \<^bold>\<lambda>x. x"
+abbreviation id :: t where "id \<equiv> \<^bold>\<lambda>x. x"  \<comment> \<open>Polymorphic identity function\<close>
 
 
 end
diff --git a/ProdProps.thy b/ProdProps.thy
deleted file mode 100644
index a68f79b..0000000
--- a/ProdProps.thy
+++ /dev/null
@@ -1,57 +0,0 @@
-(*  Title:  HoTT/ProdProps.thy
-    Author: Josh Chen
-
-Properties of the dependent product
-*)
-
-theory ProdProps
-  imports
-    HoTT_Methods
-    Prod
-begin
-
-
-section \<open>Composition\<close>
-
-text "
-  The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter.
-"
-
-lemma compose_assoc:
-  assumes "A: U i" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D x"
-  shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)"
-proof (subst (0 1 2 3) compose_def)
-  show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)"
-  proof (subst Prod_eq)
-    \<comment> \<open>Todo: set the Simplifier (or other simplification methods) up to use \<open>Prod_eq\<close>!\<close>
-    
-    show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
-    proof compute
-      show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
-      proof compute
-        show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (routine lems: assms)
-      qed
-      show "\<And>x. x: B \<Longrightarrow> h`(g`x): D (g`x)" by (routine lems: assms)
-    qed (routine lems: assms)
-  qed fact
-qed
-
-
-lemma compose_comp:
-  assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x"
-  shows "(\<^bold>\<lambda>x. c x) \<circ> (\<^bold>\<lambda>x. b x) \<equiv> \<^bold>\<lambda>x. c (b x)"
-proof (subst compose_def, subst Prod_eq)
-  show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c x)`((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a"
-  proof compute
-    show "\<And>a. a: A \<Longrightarrow> c ((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a"
-    by (derive lems: assms)
-  qed (routine lems: assms)
-qed (derive lems: assms)
-
-
-text "Set up the \<open>compute\<close> method to automatically simplify function compositions."
-
-lemmas compose_comp [comp]
-
-
-end
-- 
cgit v1.2.3


From 76ac8ed82317f3f62f26ecc88f412c61004bcffa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 13:13:55 +0200
Subject: Reorganizing theories

---
 Coprod.thy       | 64 +++++++++++++++++++++-----------------------------------
 Empty.thy        | 22 ++++++++-----------
 HoTT.thy         |  2 +-
 HoTT_Base.thy    | 25 ++++++++++++----------
 HoTT_Methods.thy | 56 +++++++++++++++++++------------------------------
 Nat.thy          | 60 ++++++++++++++++++++++++----------------------------
 Proj.thy         | 56 ++++++++++++++++++-------------------------------
 Sum.thy          | 57 ++++++++++++++++++++-----------------------------
 Unit.thy         | 32 +++++++++++++---------------
 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
-- 
cgit v1.2.3


From 8e4ca285430c7bcdabbd4ea34da38e0770f4a832 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 15:33:42 +0200
Subject: Tweak proof

---
 HoTT_Methods.thy |  4 ++--
 Proj.thy         | 13 +++++--------
 2 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 9849195..411176e 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -50,10 +50,10 @@ method derive uses lems = (routine add: lems | compute comp: lems)+
 
 section \<open>Induction\<close>
 
-text "
+text \<open>
   Placeholder section for the automation of induction, i.e. using the elimination rules.
   At the moment one must directly apply them with \<open>rule X_elim\<close>.
-"
+\<close>
 
 
 end
diff --git a/Proj.thy b/Proj.thy
index f272224..e76e8d3 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -7,10 +7,7 @@ Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent
 *)
 
 theory Proj
-imports
-  HoTT_Methods
-  Prod
-  Sum
+imports HoTT_Methods Prod Sum
 
 begin
 
@@ -28,12 +25,12 @@ unfolding fst_def by compute (derive lems: assms)
 
 lemma snd_type:
   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)
-  
+unfolding snd_def proof (derive lems: assms)
+  show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> fst p: A" using assms(1-2) by (rule fst_type)
+
   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
+qed
 
 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"
-- 
cgit v1.2.3


From 49c008ef405ab8d8229ae1d5b0737339ee46e576 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 16:00:56 +0200
Subject: Clean up Equal.thy + some other tweaks

---
 Equal.thy     | 59 ++++++++++++++++++++++-------------------------------------
 HoTT.thy      |  7 +++++--
 HoTT_Base.thy |  2 +-
 3 files changed, 28 insertions(+), 40 deletions(-)

diff --git a/Equal.thy b/Equal.thy
index 7b6acb5..f9bc223 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -1,66 +1,51 @@
-(*  Title:  HoTT/Equal.thy
-    Author: Josh Chen
+(*
+Title:  Equal.thy
+Author: Joshua Chen
+Date:   2018
 
 Equality type
 *)
 
 theory Equal
-  imports HoTT_Base
+imports HoTT_Base HoTT_Methods
+
 begin
 
 
-section \<open>Constants and syntax\<close>
+section \<open>Basic definitions\<close>
 
 axiomatization
-  Equal :: "[t, t, t] \<Rightarrow> t" and
-  refl :: "t \<Rightarrow> t" and
+  Equal    :: "[t, t, t] \<Rightarrow> t" and
+  refl     :: "t \<Rightarrow> t" and
   indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>=)")
 
 syntax
-  "_EQUAL" :: "[t, t, t] \<Rightarrow> t"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
-  "_EQUAL_ASCII" :: "[t, t, t] \<Rightarrow> t"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
+  "_equal" :: "[t, t, t] \<Rightarrow> t"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
+  "_equal_ascii" :: "[t, t, t] \<Rightarrow> t"  ("(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 where
+  Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" and
 
-section \<open>Type rules\<close>
+  Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" and
 
-axiomatization where
-  Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i"
-and
-  Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a"
-and
   Equal_elim: "\<lbrakk>
+    p: x =\<^sub>A y;
     x: A;
     y: A;
-    p: x =\<^sub>A y;
-    \<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 =\<^sub>A y \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>= f p : C x y p"
-and
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
+
   Equal_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 =\<^sub>A y \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>= f (refl a) \<equiv> f a"
-
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
-text "Admissible inference rules for equality type formation:"
-
-axiomatization where
-  Equal_wellform1: "a =\<^sub>A b: U i \<Longrightarrow> A: U i"
-and
-  Equal_wellform2: "a =\<^sub>A b: U i \<Longrightarrow> a: A"
-and
-  Equal_wellform3: "a =\<^sub>A b: U i \<Longrightarrow> b: A"
-
-
-text "Rule attribute declarations:"
-
-lemmas Equal_comp [comp]
-lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
+lemmas Equal_comp [comp]
 
 
 end
diff --git a/HoTT.thy b/HoTT.thy
index 3f2d475..e2a7e35 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -6,7 +6,6 @@ Homotopy type theory
 
 theory HoTT
 imports
-
 (* Basic theories *)
 HoTT_Base
 HoTT_Methods
@@ -22,18 +21,22 @@ Unit
 
 (* Derived definitions and properties *)
 EqualProps
-ProdProps
 Proj
 
 begin
 
+
 lemmas forms =
   Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
+
 lemmas intros =
   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 =
   Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine
 
+
 end
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index efc6182..17e3142 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -77,7 +77,7 @@ Declare named theorems to be used by proof methods defined in @{file HoTT_Method
 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>
 
-(* Todo: Set up the simplifier! *)
+(* Todo: Set up the Simplifier! *)
 
 
 end
-- 
cgit v1.2.3


From dcf87145a1059659099bbecde55973de0d36d43f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 03:04:37 +0200
Subject: Theories fully reorganized. Well-formedness rules removed. New
 methods etc.

---
 Equal.thy        |  10 +-
 EqualProps.thy   | 398 ++++++++++++-------------------------------------------
 HoTT_Base.thy    |   4 +-
 HoTT_Methods.thy |  18 +--
 Prod.thy         |   5 +-
 Univalence.thy   | 194 ++++++++-------------------
 6 files changed, 158 insertions(+), 471 deletions(-)

diff --git a/Equal.thy b/Equal.thy
index f9bc223..7a31e37 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -7,7 +7,7 @@ Equality type
 *)
 
 theory Equal
-imports HoTT_Base HoTT_Methods
+imports HoTT_Base
 
 begin
 
@@ -36,13 +36,13 @@ axiomatization where
     p: x =\<^sub>A y;
     x: A;
     y: A;
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
+    \<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 =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
 
   Equal_comp: "\<lbrakk>
     a: A;
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f 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 =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
 lemmas Equal_comp [comp]
diff --git a/EqualProps.thy b/EqualProps.thy
index 19c788c..abb2623 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -1,361 +1,137 @@
-(*  Title:  HoTT/EqualProps.thy
-    Author: Josh Chen
+(*
+Title:  EqualProps.thy
+Author: Joshua Chen
+Date:   2018
 
 Properties of equality
 *)
 
 theory EqualProps
-  imports
-    HoTT_Methods
-    Equal
-    Prod
+imports HoTT_Methods Equal Prod
+
 begin
 
 
-section \<open>Symmetry / Path inverse\<close>
-
-definition inv :: "t \<Rightarrow> t"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p"
-
-text "
-  In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use.
-  The proof is finished with a standard application of the relevant type rules.
-"
-
-lemma inv_type:
-  assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
-unfolding inv_def
-by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms)
-  \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close>
-
-text "
-  The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules.
-  (If viewing this inside Isabelle, place the cursor after the \<open>proof\<close> statement and observe the second subgoal.)
-"
-
-lemma inv_comp:
-  assumes "A : U i " and "a : A" shows "(refl a)\<inverse> \<equiv> refl a"
-unfolding inv_def
-proof compute
-  show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
-qed (routine lems: assms)
-
-
-section \<open>Transitivity / Path composition\<close>
-
-text "
-  Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>.
-"
-
-definition rpathcomp :: t where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
-
-text "
-  More complicated proofs---the nested path inductions require more explicit step-by-step rule applications:
-"
-
-lemma rpathcomp_type:
-  assumes "A: U i"
-  shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-unfolding rpathcomp_def
-proof
-  fix x assume 1: "x: A"
-  show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-  proof
-    fix y assume 2: "y: A"
-    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-    proof
-      fix p assume 3: "p: x =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=x and ?y=y])
-        show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z"
-            show "ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm)
-          qed (routine lems: assms)
-        qed (rule assms)
-      qed (routine lems: assms 1 2 3)
-    qed (routine lems: assms 1 2)
-  qed (rule assms)
-qed fact
-
-corollary
-  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
-  shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z"
-  by (routine lems: assms rpathcomp_type)
-
-text "
-  The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule.
-"
-
-lemma rpathcomp_comp:
-  assumes "A: U i" and "a: A"
-  shows "rpathcomp`a`a`(refl a)`a`(refl a) \<equiv> refl a"
-unfolding rpathcomp_def
-proof compute
-  fix x assume 1: "x: A"
-  show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-  proof
-    fix y assume 2: "y: A"
-    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-    proof
-      fix p assume 3: "p: x =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=x and ?y=y])
-        show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            fix u z assume asm: "u: A" "z: A"
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm)
-          qed (routine lems: assms)
-        qed (rule assms)
-      qed (routine lems: assms 1 2 3)
-    qed (routine lems: assms 1 2)
-  qed (rule assms)
-
-  next show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \<equiv> refl a"
-  proof compute
-    fix y assume 1: "y: A"
-    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)"
-    proof
-      fix p assume 2: "p: a =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=a and ?y=y])
-        fix u assume 3: "u: A"
-        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          fix z assume 4: "z: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4)
-          qed (routine lems: assms 3 4)
-        qed fact
-      qed (routine lems: assms 1 2)
-    qed (routine lems: assms 1)
-    
-    next show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \<equiv> refl a"
-    proof compute
-      fix p assume 1: "p: a =\<^sub>A a"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A z \<rightarrow> a =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=a and ?y=a])
-        fix u assume 2: "u: A"
-        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          fix z assume 3: "z: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3)
-          qed (routine lems: assms 2 3)
-        qed fact
-      qed (routine lems: assms 1)
-      
-      next show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \<equiv> refl a"
-      proof compute
-        fix u assume 1: "u: A"
-        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          fix z assume 2: "z: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2)
-          qed (routine lems: assms 1 2)
-        qed fact
-        
-        next show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`(refl a) \<equiv> refl a"
-        proof compute
-          fix a assume 1: "a: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
-          proof
-            show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a"
-            by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1)
-          qed (routine lems: assms 1)
-          
-          next show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`(refl a) \<equiv> refl a"
-          proof compute
-            show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a"
-            by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms)
-            show "ind\<^sub>= refl (refl a) \<equiv> refl a"
-            proof compute
-              show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" ..
-            qed (routine lems: assms)
-          qed (routine lems: assms)
-        qed fact
-      qed (routine lems: assms)
-    qed (routine lems: assms)
-  qed fact
-qed fact
-
-
-text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead."
-
-axiomatization pathcomp :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 120) where
-  pathcomp_def: "\<lbrakk>
-    A: U i;
-    x: A; y: A; z: A;
-    p: x =\<^sub>A y; q: y =\<^sub>A z
-  \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q"
+section \<open>Symmetry of equality/Path inverse\<close>
 
+definition inv :: "t \<Rightarrow> t"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl x) p"
 
-lemma pathcomp_type:
-  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
-  shows "p \<bullet> q: x =\<^sub>A z"
+lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =\<^sub>A y\<rbrakk> \<Longrightarrow> p\<inverse>: y =\<^sub>A x"
+unfolding inv_def by (elim Equal_elim) routine
 
-proof (subst pathcomp_def)
-  show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
-qed (routine lems: assms rpathcomp_type)
+lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (refl a)\<inverse> \<equiv> refl a"
+unfolding inv_def by compute routine
 
 
-lemma pathcomp_comp:
-  assumes "A : U i" and "a : A" shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
-by (subst pathcomp_def) (routine lems: assms rpathcomp_comp)
+section \<open>Transitivity of equality/Path composition\<close>
 
+text \<open>
+Composition function, of type @{term "x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"} polymorphic over @{term A}, @{term x}, @{term y}, and @{term z}.
+\<close>
 
-lemmas inv_type [intro]
-lemmas pathcomp_type [intro]
+definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
 
-lemmas inv_comp [comp]
-lemmas pathcomp_comp [comp]
+syntax "_pathcomp" :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 120)
+translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
 
+lemma pathcomp_type:
+  assumes "A: U i" and "x: A" "y: A" "z: A"
+  shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"
+unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms)
 
-section \<open>Weak higher groupoid structure of types\<close>
+corollary pathcomp_trans:
+  assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  shows "p \<bullet> q: x =\<^sub>A z"
+by (routine add: assms pathcomp_type)
 
-schematic_goal whg1a:
+lemma pathcomp_comp:
+  assumes "A: U i" and "a: A"
+  shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
+unfolding pathcomp_def proof compute
+  show "(ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) (refl a))`(refl a) \<equiv> refl a"
+  proof compute
+    show "\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q): a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
+    by (routine add: assms)
+
+    show "(\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q))`(refl a) \<equiv> refl a"
+    proof compute
+      show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>x. refl x) q: a =\<^sub>A a" by (routine add: assms)
+    qed (derive lems: assms)
+  qed (routine add: assms)
+
+  show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) p: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
+  by (routine add: assms)
+qed (routine add: assms)
+
+
+section \<open>Higher groupoid structure of types\<close>
+
+schematic_goal pathcomp_right_id:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows "?a: p =[x =\<^sub>A y] (p \<bullet> (refl(y)))"
-proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))"
-  by compute (routine lems: assms)
-qed (routine lems: assms)
+  shows "?a: p \<bullet> (refl y) =[x =\<^sub>A y] p"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])  \<comment> \<open>@{method elim} does not seem to work with schematic goals.\<close>
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms pathcomp_comp)
+qed (routine add: assms pathcomp_type)
 
-schematic_goal whg1b:
+schematic_goal pathcomp_left_id:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows "?a: p =[x =\<^sub>A y] (refl(x) \<bullet> p)"
+  shows "?a: (refl x) \<bullet> p =[x =\<^sub>A y] p"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))"
-  by compute (routine lems: assms)
-qed (routine lems: assms)
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms pathcomp_comp)
+qed (routine add: assms pathcomp_type)
 
-schematic_goal whg2a:
+schematic_goal pathcomp_left_inv:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): ((refl(x))\<inverse> \<bullet> refl(x)) =[x =\<^sub>A x] refl(x)"
-  by (compute | routine lems: assms)+
-qed (routine lems: assms)+
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse> \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms inv_comp pathcomp_comp)
+qed (routine add: assms inv_type pathcomp_type)
 
-schematic_goal whg2b:
+schematic_goal pathcomp_right_inv:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x) \<bullet> (refl(x))\<inverse>) =[x =\<^sub>A x] refl(x)"
-  by (compute | routine lems: assms)+
-qed (routine lems: assms)+
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x)\<inverse> =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms inv_comp pathcomp_comp)
+qed (routine add: assms inv_type pathcomp_type)
 
-schematic_goal whg3:
+schematic_goal inv_involutive:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x))\<inverse>\<inverse> =[x =\<^sub>A x] refl(x)"
-  by (compute | routine lems: assms)+
-qed (routine lems: assms)
-
-
-lemma assumes "A: U(i)" shows "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x"
-by (rule Prod_atomize[where ?A=A and ?B="\<lambda>x. x =\<^sub>A x"]) (routine lems: assms)
-
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse>\<inverse> =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms inv_comp)
+qed (routine add: assms inv_type)
 
-schematic_goal
+schematic_goal pathcomp_assoc:
   assumes
-    "A: U(i)" and
-    "x: A" "y: A" "z: A" "w: A" and
+    "A: U(i)"
+    "x: A" "y: A" "z: A" "w: A"
     "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
   shows
     "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  fix y assume "y: A"
-  show "refl(q \<bullet> r): refl(y) \<bullet> (q \<bullet> r) =[y =\<^sub>A w] (refl(y) \<bullet> q) \<bullet> r"
-  proof (compute lems: whg1b)
-  
-
-section \<open>Higher groupoid structure of types\<close>
-
-lemma
-  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> (refl y)" and
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \<bullet> p"
-
-proof -
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> (refl y)"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] (refl x) \<bullet> p"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-qed
-
-
-lemma
-  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" and
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)"
-
-proof -
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-qed
-
-
-lemma
-  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
-by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)
-
-text "Next we construct a proof term of associativity of path composition."
-
-schematic_goal
-  assumes
-    "A: U i"
-    "x: A" "y: A" "z: A" "w: A"
-    "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
-  shows
-    "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A z] (p \<bullet> q) \<bullet> r"
-
-apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y])
-apply (rule assms)+
-\<comment> \<open>Continue by substituting \<open>refl x \<bullet> q = q\<close> etc.\<close>
-sorry
+  fix x assume "x: A"
+  show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r"
+  \<comment> \<open>This requires substitution of *propositional* equality. \<close>
+  sorry
+  oops
 
 
 section \<open>Transport\<close>
 
-definition transport :: "t \<Rightarrow> t" where
-  "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p"
+definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>_. (\<^bold>\<lambda>x. x)) p"
 
-text "Note that \<open>transport\<close> is a polymorphic function in our formulation."
+text \<open>Note that @{term transport} is a polymorphic function in our formulation.\<close>
 
-lemma transport_type:
-  assumes
-    "A: U i" "P: A \<longrightarrow> U i"
-    "x: A" "y: A"
-    "p: x =\<^sub>A y"
-  shows "transport p: P x \<rightarrow> P y"
-unfolding transport_def
-by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms)
-
-lemma transport_comp:
-  assumes "A: U i" and "x: A"
-  shows "transport (refl x) \<equiv> id"
-unfolding transport_def by (derive lems: assms)
+lemma transport_type: "\<lbrakk>p: x =\<^sub>A y; x: A; y: A; A: U i; P: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> transport p: P x \<rightarrow> P y"
+unfolding transport_def by (elim Equal_elim) routine
+
+lemma transport_comp: "\<lbrakk>A: U i; x: A\<rbrakk> \<Longrightarrow> transport (refl x) \<equiv> id"
+unfolding transport_def by derive
 
 
 end
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 17e3142..7453883 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -7,9 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty
 *)
 
 theory HoTT_Base
-imports
-  Pure
-  "HOL-Eisbach.Eisbach"
+imports Pure "HOL-Eisbach.Eisbach"
 
 begin
 
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 411176e..8929f69 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -3,14 +3,11 @@ Title:  HoTT_Methods.thy
 Author: Joshua Chen
 Date:   2018
 
-Method setup for the HoTT logic. Relies heavily on Eisbach.
+Method setup for the HoTT logic.
 *)
 
 theory HoTT_Methods
-imports
-  "HOL-Eisbach.Eisbach"
-  "HOL-Eisbach.Eisbach_Tools"
-  HoTT_Base
+imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 
 begin
 
@@ -43,16 +40,19 @@ Premises of the rule(s) applied are added as new subgoals.
 
 section \<open>Derivation search\<close>
 
-text \<open>Combine @{method routine} and @{method compute} to search for derivations of judgments.\<close>
+text \<open>
+Combine @{method routine} and @{method compute} to search for derivations of judgments.
+Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}.
+\<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems)+
+method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+
 
 
 section \<open>Induction\<close>
 
 text \<open>
-  Placeholder section for the automation of induction, i.e. using the elimination rules.
-  At the moment one must directly apply them with \<open>rule X_elim\<close>.
+Placeholder section for the automation of induction, i.e. using the elimination rules.
+At the moment one must directly apply them with \<open>rule X_elim\<close>.
 \<close>
 
 
diff --git a/Prod.thy b/Prod.thy
index db18454..4aa7119 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -17,7 +17,7 @@ section \<open>Basic definitions\<close>
 axiomatization
   Prod   :: "[t, tf] \<Rightarrow> t" and
   lambda :: "(t \<Rightarrow> t) \<Rightarrow> t"  (binder "\<^bold>\<lambda>" 30) and
-  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`/_)" [60, 61] 60)  \<comment> \<open>Application binds tighter than abstraction.\<close>
+  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`/_)" [105, 106] 105)  \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
   "_prod" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Prod>_:_./ _)" 30)
@@ -43,7 +43,7 @@ axiomatization where
 
   Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and
 
-  Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and
+  Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and
 
   Prod_uniq: "f: \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. f`x \<equiv> f" and
 
@@ -68,6 +68,7 @@ lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 section \<open>Additional definitions\<close>
 
 definition compose :: "[t, t] \<Rightarrow> t"  (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)"
+
 syntax "_compose" :: "[t, t] \<Rightarrow> t"  (infixr "\<circ>" 110)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
diff --git a/Univalence.thy b/Univalence.thy
index 001ee33..3c9b520 100644
--- a/Univalence.thy
+++ b/Univalence.thy
@@ -1,176 +1,88 @@
-(*  Title:  HoTT/Univalence.thy
-    Author: Joshua Chen
+(*
+Title:  Univalence.thy
+Author: Joshua Chen
+Date:   2018
 
 Definitions of homotopy, equivalence and the univalence axiom.
 *)
 
 theory Univalence
-imports
-  HoTT_Methods
-  EqualProps
-  ProdProps
-  Sum
+imports HoTT_Methods EqualProps Prod Sum
 
 begin
 
 
 section \<open>Homotopy and equivalence\<close>
 
-axiomatization homotopic :: "[t, t] \<Rightarrow> t"  (infix "~" 100) where
-  homotopic_def: "\<lbrakk>
-    f: \<Prod>x:A. B x;
-    g: \<Prod>x:A. B x
-  \<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"
+definition homotopic :: "[t, tf, t, t] \<Rightarrow> t" where "homotopic A B f g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"
 
-axiomatization isequiv :: "t \<Rightarrow> t" where
-  isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)"
+syntax "_homotopic" :: "[t, idt, t, t, t] \<Rightarrow> t"  ("(1_ ~[_:_. _]/ _)" [101, 0, 0, 0, 101] 100)
+translations "f ~[x:A. B] g" \<rightleftharpoons> "CONST homotopic A (\<lambda>x. B) f g"
 
-definition equivalence :: "[t, t] \<Rightarrow> t"  (infix "\<simeq>" 100)
-  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f"
-
-
-text "The identity function is an equivalence:"
-
-lemma isequiv_id:
-  assumes "A: U i" and "id: A \<rightarrow> A"
-  shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id"
-proof (derive lems: assms isequiv_def homotopic_def)
-  fix g assume asm: "g: A \<rightarrow> A"
-  show "id \<circ> g: A \<rightarrow> A"
-    unfolding compose_def by (routine lems: asm assms)
-
-  show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i"
-    unfolding compose_def by (routine lems: asm assms)
-  next
-  
-  show "<\<^bold>\<lambda>x. x, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~ id"
-    unfolding compose_def by (derive lems: assms homotopic_def)
-
-  show "<\<^bold>\<lambda>x. x, lambda refl>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~ id"
-    unfolding compose_def by (derive lems: assms homotopic_def)
-qed (rule assms)
+declare homotopic_def [comp]
 
+definition isequiv :: "[t, t, t] \<Rightarrow> t"  ("(3isequiv[_, _]/ _)") where
+  "isequiv[A, B] f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~[x:A. A] id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~[x:B. B] id)"
 
-text "We use the following lemma in a few proofs:"
+text \<open>
+The meanings of the syntax defined above are:
+\<^item> @{term "f ~[x:A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "\<Prod>x:A. B x"}.
+\<^item> @{term "isequiv[A, B] f"} expresses that the non-dependent function @{term f} of type @{term "A \<rightarrow> B"} is an equivalence.
+\<close>
 
-lemma isequiv_type:
-  assumes "A: U i" and "B: U i" and "f: A \<rightarrow> B"
-  shows "isequiv f: U i"
-  by (derive lems: assms isequiv_def homotopic_def compose_def)
-
-
-text "The equivalence relation \<open>\<simeq>\<close> is symmetric:"
+definition equivalence :: "[t, t] \<Rightarrow> t"  (infix "\<simeq>" 100)
+  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv[A, B] f"
+
+lemma id_isequiv:
+  assumes "A: U i" "id: A \<rightarrow> A"
+  shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id"
+unfolding isequiv_def proof (routine add: assms)
+  show "\<And>g. g: A \<rightarrow> A \<Longrightarrow> id \<circ> g ~[x:A. A] id: U i" by (derive lems: assms)
+  show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~[x:A. A] id" by (derive lems: assms)
+  show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~[x:A. A] id" by (derive lems: assms)
+qed
 
-lemma equiv_sym:
+lemma equivalence_symm:
   assumes "A: U i" and "id: A \<rightarrow> A"
   shows "<id, <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>>: A \<simeq> A"
 unfolding equivalence_def proof
-  show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" using assms by (rule isequiv_id)
-  
-  fix f assume "f: A \<rightarrow> A"
-  with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type)
-qed (rule assms)
+  show "\<And>f. f: A \<rightarrow> A \<Longrightarrow> isequiv[A, A] f: U i" by (derive lems: assms isequiv_def)
+  show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id" using assms by (rule id_isequiv)
+qed fact
 
 
-section \<open>idtoeqv and the univalence axiom\<close>
+section \<open>idtoeqv\<close>
 
-definition idtoeqv :: t
-  where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"
+definition idtoeqv :: t where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"
 
-
-text "We prove that equal types are equivalent. The proof is long and uses universes."
+text \<open>We prove that equal types are equivalent. The proof involves universe types.\<close>
 
 theorem
   assumes "A: U i" and "B: U i"
   shows "idtoeqv: (A =[U i] B) \<rightarrow> A \<simeq> B"
-unfolding idtoeqv_def equivalence_def
-proof
-  fix p assume "p: A =[U i] B"
-  show "<transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>: \<Sum>f: A \<rightarrow> B. isequiv f"
-  proof
-    { fix f assume "f: A \<rightarrow> B"
-    with assms show "isequiv f: U i" by (rule isequiv_type)
-    }
-    
-    show "transport p: A \<rightarrow> B"
-    proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="Suc i"])
-      show "\<And>x. x: U i \<Longrightarrow> x: U (Suc i)" by cumulativity
-      show "U i: U (Suc i)" by hierarchy
-    qed fact+
+unfolding idtoeqv_def equivalence_def proof (routine add: assms)
+  show *: "\<And>f. f: A \<rightarrow> B \<Longrightarrow> isequiv[A, B] f: U i"
+  unfolding isequiv_def by (derive lems: assms)
+
+  show "\<And>p. p: A =[U i] B \<Longrightarrow> transport p: A \<rightarrow> B"
+  by (derive lems: assms transport_type[where ?i="Suc i"])
+  \<comment> \<open>Instantiate @{thm transport_type} with a suitable universe level here...\<close>
+
+  show "\<And>p. p: A =[U i] B \<Longrightarrow> ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv[A, B] (transport p)"
+  proof (elim Equal_elim)
+    show "\<And>T. T: U i \<Longrightarrow> <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[T, T] (transport (refl T))"
+    by (derive lems: transport_comp[where ?i="Suc i" and ?A="U i"] id_isequiv)
+    \<comment> \<open>...and also here.\<close>
     
-    show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)"
-    proof (rule Equal_elim[where ?C="\<lambda>_ _ p. isequiv (transport p)"])
-      fix A assume asm: "A: U i"
-      show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv (transport (refl A))"
-      proof (derive lems: isequiv_def)
-        show "transport (refl A): A \<rightarrow> A"
-          unfolding transport_def
-          by (compute lems: Equal_comp[where ?A="U i" and ?C="\<lambda>_ _ _. A \<rightarrow> A"]) (derive lems: asm)
-        
-        show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
-                (\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times>
-                (\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)"
-        proof (subst (1 2) transport_comp)
-          show "U i: U (Suc i)" by (rule U_hierarchy) rule
-          show "U i: U (Suc i)" by (rule U_hierarchy) rule
-          
-          show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
-                  (\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)"
-          proof
-            show "\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id: U i"
-            proof (derive lems: asm homotopic_def)
-              fix g assume asm': "g: A \<rightarrow> A"
-              show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
-              show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
-            qed (routine lems: asm)
-
-            show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. id \<circ> g ~ id"
-            proof
-              fix g assume asm': "g: A \<rightarrow> A"
-              show "id \<circ> g ~ id: U i"
-              proof (derive lems: homotopic_def)
-                show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
-                show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
-              qed (routine lems: asm)
-              next
-              show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
-              proof compute
-                show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
-              qed (rule asm)
-            qed (routine lems: asm)
-
-            show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. g \<circ> id ~ id"
-            proof
-              fix g assume asm': "g: A \<rightarrow> A"
-              show "g \<circ> id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def)
-              next
-              show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
-              proof compute
-                show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
-              qed (rule asm)
-            qed (routine lems: asm)
-          qed
-        qed fact+
-      qed
-      next
-      
-      fix A' B' p' assume asm:  "A': U i" "B': U i" "p': A' =[U i] B'"
-      show "isequiv (transport p'): U i"
-      proof (rule isequiv_type)
-        show "transport p': A' \<rightarrow> B'" by (derive lems: asm transport_def)
-      qed fact+
-    qed fact+
-  qed
-  next
-
-  show "A =[U i] B: U (Suc i)" proof (derive lems: assms, (rule U_hierarchy, rule lt_Suc)?)+
-qed
+    show "\<And>A B p. \<lbrakk>A: U i; B: U i; p: A =[U i] B\<rbrakk> \<Longrightarrow> isequiv[A, B] (transport p): U i"
+    unfolding isequiv_def by (derive lems: assms transport_type)
+  qed fact+
+qed (derive lems: assms)
 
 
-text "The univalence axiom."
+section \<open>The univalence axiom\<close>
 
-axiomatization univalence :: t where
-  UA: "univalence: isequiv idtoeqv"
+axiomatization univalence :: "[t, t] \<Rightarrow> t" where UA: "univalence A B: isequiv[A, B] idtoeqv"
 
 
 end
-- 
cgit v1.2.3


From 6857e783fa5cb91f058be322a18fb9ea583f2aad Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 11:38:54 +0200
Subject: Overhaul of the theory presentations. New methods in HoTT_Methods.thy
 for handling universes. Commit for release 0.1.0!

---
 Coprod.thy           |   1 +
 Empty.thy            |   1 +
 Equal.thy            |   1 +
 HoTT.thy             |   9 +++--
 HoTT_Base.thy        |  29 ++++++++-------
 HoTT_Methods.thy     |  25 ++++++++++++-
 Nat.thy              |   1 +
 Prod.thy             |   1 +
 Sum.thy              |   1 +
 Unit.thy             |   1 +
 ex/HoTT book/Ch1.thy |  47 +++++++++++------------
 ex/Methods.thy       |  73 ++++++++++++------------------------
 ex/Synthesis.thy     |  94 ++++++++++++++++++----------------------------
 tests/Subgoal.thy    |  63 -------------------------------
 tests/Test.thy       | 103 +++++++++++++++++++++++----------------------------
 15 files changed, 177 insertions(+), 273 deletions(-)
 delete mode 100644 tests/Subgoal.thy

diff --git a/Coprod.thy b/Coprod.thy
index d97228e..431e103 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -42,6 +42,7 @@ where
     \<And>x. x: A \<Longrightarrow> c x: C (inl x);
     \<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_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
 
diff --git a/Empty.thy b/Empty.thy
index 3060867..ee11045 100644
--- a/Empty.thy
+++ b/Empty.thy
@@ -20,6 +20,7 @@ where
 
   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
 
 
diff --git a/Equal.thy b/Equal.thy
index 7a31e37..19e3939 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -44,6 +44,7 @@ axiomatization where
     \<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 =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
+lemmas Equal_form [form]
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
 lemmas Equal_comp [comp]
 
diff --git a/HoTT.thy b/HoTT.thy
index e2a7e35..0e7a674 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,5 +1,7 @@
-(*  Title:  HoTT/HoTT.thy
-    Author: Josh Chen
+(*
+Title:  HoTT.thy
+Author: Joshua Chen
+Date:   2018
 
 Homotopy type theory
 *)
@@ -26,8 +28,7 @@ Proj
 begin
 
 
-lemmas forms =
-  Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
+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
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 7453883..2ad0ac5 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -7,7 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty
 *)
 
 theory HoTT_Base
-imports Pure "HOL-Eisbach.Eisbach"
+imports Pure
 
 begin
 
@@ -18,17 +18,14 @@ typedecl t  \<comment> \<open>Type of object types and terms\<close>
 typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
 
 axiomatization
-  O :: ord and
+  O   :: ord and
   Suc :: "ord \<Rightarrow> ord" and
-  lt :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999)
+  lt  :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999) and
+  leq :: "[ord, ord] \<Rightarrow> prop"  (infix "\<le>" 999)
 where
   lt_Suc [intro]: "n < (Suc n)" and
   lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
-  Suc_monotone [simp]: "m < n \<Longrightarrow> (Suc m) < (Suc n)"
-
-method proveSuc = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
-
-text \<open>Method @{method proveSuc} proves statements of the form \<open>n < (Suc (... (Suc n) ...))\<close>.\<close>
+  leq_min [intro]: "O \<le> n"
 
 
 section \<open>Judgment\<close>
@@ -42,15 +39,15 @@ axiomatization
   U :: "ord \<Rightarrow> t"
 where
   U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
-  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j"
+  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and
+  U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
 text \<open>
 Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
 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>
+@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}.
+\<close>
 
 
 section \<open>Type families\<close>
@@ -68,11 +65,15 @@ type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<
 section \<open>Named theorems\<close>
 
 named_theorems comp
+named_theorems form
 
 text \<open>
 Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
-@{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.
+
+@{attribute comp} declares computation rules, which 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.
+
+@{attribute form} declares type formation rules.
+These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
 \<close>
 
 (* Todo: Set up the Simplifier! *)
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 8929f69..f0cee6c 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -12,6 +12,26 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 begin
 
 
+section \<open>Handling universes\<close>
+
+method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
+
+method hierarchy = (rule U_hierarchy, provelt)
+
+method cumulativity declares form = (
+  ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) |
+  ((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
+)
+
+text \<open>
+Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form
+\<^item> \<open>n < (Suc (... (Suc n) ...))\<close>,
+\<^item> \<open>U i: U (Suc (... (Suc i) ...))\<close>, and
+\<^item> @{prop "A: U i \<Longrightarrow> A: U j"}, where @{prop "i \<le> j"}
+respectively.
+\<close>
+
+
 section \<open>Deriving typing judgments\<close>
 
 method routine uses add = (assumption | rule add | rule)+
@@ -38,14 +58,15 @@ Method @{method compute} performs single-step simplifications, using any rules d
 Premises of the rule(s) applied are added as new subgoals.
 \<close>
 
+
 section \<open>Derivation search\<close>
 
 text \<open>
 Combine @{method routine} and @{method compute} to search for derivations of judgments.
-Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}.
+Also handle universes using @{method hierarchy} and @{method cumulativity}.
 \<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+
+method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
 
 section \<open>Induction\<close>
diff --git a/Nat.thy b/Nat.thy
index 46b1af5..8a55852 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -41,6 +41,7 @@ where
     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_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
 
diff --git a/Prod.thy b/Prod.thy
index 4aa7119..f90ee9c 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -61,6 +61,7 @@ Note that this is a separate rule from function extensionality.
 Note that the bold lambda symbol \<open>\<^bold>\<lambda>\<close> used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation).
 \<close>
 
+lemmas Prod_form [form]
 lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
diff --git a/Sum.thy b/Sum.thy
index 422e01b..463a9d4 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -51,6 +51,7 @@ axiomatization where
 
   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_form [form]
 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim
 lemmas Sum_comp [comp]
 
diff --git a/Unit.thy b/Unit.thy
index 61c6439..7c221f0 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -25,6 +25,7 @@ where
 
   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]
 
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index a577fca..263f43d 100644
--- a/ex/HoTT book/Ch1.thy	
+++ b/ex/HoTT book/Ch1.thy	
@@ -1,55 +1,50 @@
-(*  Title:  HoTT/ex/HoTT book/Ch1.thy
-    Author: Josh Chen
+(*
+Title:  ex/HoTT book/Ch1.thy
+Author: Josh Chen
+Date:   2018
 
 A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
 *)
 
 theory Ch1
-  imports "../../HoTT"
+imports "../../HoTT"
+
 begin
 
 chapter \<open>HoTT Book, Chapter 1\<close>
 
-section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
+section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
 
-text "Propositional uniqueness principle:"
+paragraph \<open>Propositional uniqueness principle.\<close>
 
 schematic_goal
-  assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
-  shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>"
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x"
+  shows "?a: p =[\<Sum>x:A. B x] <fst p, snd p>"
 
-text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:"
+text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
 
 proof (rule Sum_elim[where ?p=p])
-  text "We just need to prove the base case; the rest will be taken care of automatically."
-
-  fix x y assume asm: "x: A" "y: B(x)" show
-    "refl(<x,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>"
-  proof (subst (0 1) comp)
-    text "
-      The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> have appropriate types.
-      The automatic proof methods have trouble picking the appropriate types, so we state them explicitly,
-    "
-    show "x: A" and "y: B(x)" by (fact asm)+
-
-    text "...twice, once each for the substitutions of \<open>fst\<close> and \<open>snd\<close>."
-    show "x: A" and "y: B(x)" by (fact asm)+
+  text \<open>We prove the base case.\<close>
+  fix x y assume asm: "x: A" "y: B x" show "refl <x,y>: <x,y> =[\<Sum>x:A. B x] <fst <x,y>, snd <x,y>>"
+  proof compute
+    show "x: A" and "y: B x" by (fact asm)+  \<comment> \<open>Hint the correct types.\<close>
 
+    text \<open>And now @{method derive} takes care of the rest.
+\<close>
   qed (derive lems: assms asm)
-
 qed (derive lems: assms)
 
 
 section \<open>Exercises\<close>
 
-text "Exercise 1.13"
+paragraph \<open>Exercise 1.13\<close>
 
-abbreviation "not" ("\<not>'(_')") where "\<not>(A) \<equiv> A \<rightarrow> \<zero>"
+abbreviation "not" ("\<not>_") where "\<not>A \<equiv> A \<rightarrow> \<zero>"
 
 text "This proof requires the use of universe cumulativity."
 
-proposition assumes "A: U(i)" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`inl(a))): \<not>(\<not>(A + \<not>(A)))"
-by (derive lems: assms U_cumulative[where ?A=\<zero> and ?i=O and ?j=i])
+proposition assumes "A: U i" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`(inl a))): \<not>(\<not>(A + \<not>A))"
+by (derive lems: assms)
 
 
 end
diff --git a/ex/Methods.thy b/ex/Methods.thy
index c78af14..09975b0 100644
--- a/ex/Methods.thy
+++ b/ex/Methods.thy
@@ -1,76 +1,49 @@
-(*  Title:  HoTT/ex/Methods.thy
-    Author: Josh Chen
+(*
+Title:  ex/Methods.thy
+Author: Joshua Chen
+Date:   2018
 
-HoTT method usage examples
+Basic HoTT method usage examples.
 *)
 
 theory Methods
-  imports "../HoTT"
-begin
+imports "../HoTT"
 
+begin
 
-text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules."
 
 lemma
   assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)"
-  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)"
-by (routine lems: assms)
-
-
-lemma
-  assumes "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z: U(i)"
-  shows
-    "A : U(i)" and
-    "B: A \<longrightarrow> U(i)" and
-    "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
-proof -
-  show
-    "A : U(i)" and
-    "B: A \<longrightarrow> U(i)" and
-    "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
-  by (derive lems: assms)
-qed
-
-
-text "Typechecking and constructing inhabitants:"
+  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w: U(i)"
+by (routine add: assms)
 
-\<comment> \<open>Correctly determines the type of the pair\<close>
+\<comment> \<open>Correctly determines the type of the pair.\<close>
 schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A"
 by routine
 
 \<comment> \<open>Finds pair (too easy).\<close>
 schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B"
-apply (rule Sum_intro)
+apply (rule intros)
 apply assumption+
 done
 
-
-text "
-  Function application.
-  The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types.
-"
-
-lemma
-  assumes "A: U(i)" "a: A"
-  shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
+\<comment> \<open>Function application. We still often have to explicitly specify types.\<close>
+lemma "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
 proof compute
   show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by routine
-qed (routine lems: assms)
-
+qed
 
-lemma
-  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)"
-  shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
-proof compute
-  show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (routine lems: assms)
+text \<open>
+The proof below takes a little more work than one might expect; it would be nice to have a one-line method or proof.
+\<close>
 
-  show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>"
+lemma "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
+proof (compute, routine)
+  show "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>y. <a,y>)`b \<equiv> <a,b>"
   proof compute
-    show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (routine lems: assms)
-  qed fact
-qed fact
+    show "\<And>b. \<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" by routine
+  qed
+qed
 
 
 end
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index a5e77ec..3ee973c 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -1,78 +1,58 @@
-(*  Title:  HoTT/ex/Synthesis.thy
-    Author: Josh Chen
+(*
+Title:  ex/Synthesis.thy
+Author: Joshua Chen
+Date:   2018
 
-Examples of synthesis.
+Examples of synthesis
 *)
 
 
 theory Synthesis
-  imports "../HoTT"
+imports "../HoTT"
+
 begin
 
 
 section \<open>Synthesis of the predecessor function\<close>
 
-text "
-  In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers.
-
-  This is also done in \<open>CTT.thy\<close>; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely.
-"
+text \<open>
+In this example we construct a predecessor function for the natural numbers.
+This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional.
+\<close>
 
-text "First we show that the property we want is well-defined."
+text \<open>First we show that the property we want is well-defined.\<close>
 
-lemma pred_welltyped: "\<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n): U(O)"
+lemma pred_welltyped: "\<Sum>pred: \<nat>\<rightarrow>\<nat>. (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n): U O"
 by routine
 
-text "
-  Now we look for an inhabitant of this type.
-  Observe that we're looking for a lambda term \<open>pred\<close> satisfying \<open>(pred`0) =\<^sub>\<nat> 0\<close> and \<open>\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n\<close>.
-  What if we require **definitional** equality instead of just propositional equality?
-"
+text \<open>
+Now we look for an inhabitant of this type.
+Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =\<^sub>\<nat> 0"} and @{term "\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n"}.
+What if we require *definitional* instead of just propositional equality?
+\<close>
 
 schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n"
 apply compute
 prefer 4 apply compute
-prefer 3 apply compute
-apply (rule Nat_routine Nat_elim | compute | assumption)+
-done
-
-text "
-  The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n\<close>.
-  We prove this has the required type and properties.
-"
-
-definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"
-
-lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by routine
-
-lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
-proof (routine lems: pred_type)
-  have *: "pred`0 \<equiv> 0" unfolding pred_def
-  proof compute
-    show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine
-    show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0"
-    proof compute
-      show "\<nat>: U(O)" ..
-    qed routine
-  qed rule
-  then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) routine
-
-  show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n"
-  unfolding pred_def proof
-    show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n)`succ(n)) =\<^sub>\<nat> n"
-    proof compute
-      show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine
-      show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) 0 (succ n) =\<^sub>\<nat> n"
-      proof compute
-        show "\<nat>: U(O)" ..
-      qed routine
-    qed rule
-  qed rule
-qed
-
-theorem
-  "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
-by (routine lems: pred_welltyped pred_type pred_props)
+apply (rule Nat_routine | compute)+
+oops
+\<comment> \<open>Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\<close>
+
+text \<open>
+The above proof finds a candidate, namely @{term "\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"}.
+We prove this has the required type and properties.
+\<close>
+
+definition pred :: t where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"
+
+lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>"
+unfolding pred_def by routine
+
+lemma pred_props: "<refl 0, \<^bold>\<lambda>n. refl n>: (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n)"
+unfolding pred_def by derive
+
+theorem "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
+by (derive lems: pred_type pred_props)
 
 
 end
diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy
deleted file mode 100644
index 82d7e5d..0000000
--- a/tests/Subgoal.thy
+++ /dev/null
@@ -1,63 +0,0 @@
-theory Subgoal
-  imports "../HoTT"
-begin
-
-
-text "
-  Proof of \<open>rpathcomp_type\<close> (see EqualProps.thy) in apply-style.
-  Subgoaling can be used to fix variables and apply the elimination rules.
-"
-
-lemma rpathcomp_type:
-  assumes "A: U(i)"
-  shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-unfolding rpathcomp_def
-apply standard
-  subgoal premises 1 for x  \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close>
-  apply standard
-    subgoal premises 2 for y
-    apply standard
-      subgoal premises 3 for p
-      apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
-        \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close>
-      prefer 4
-        apply standard
-          apply (rule Prod_intro)
-            subgoal premises 4 for u z q
-            apply (rule Equal_elim[where ?x=u and ?y=z])
-            apply (routine lems: assms 4)
-            done
-          apply (routine lems: assms 1 2 3)
-      done
-    apply (routine lems: assms 1 2)
-    done
-  apply fact
-  done
-apply fact
-done
-
-
-text "
-  \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs.
-  This is the same thing as being unable to start a ``sub schematic-goal'' inside an ongoing proof.
-
-  This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact.
-"
-
-schematic_goal rpathcomp_synthesis:
-  assumes "A: U(i)"
-  shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-
-text "
-  Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below.
-"
-
-apply (rule intros)
-  apply (rule intros)
-    apply (rule intros)
-      subgoal 123 for x y p
-      apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
-      oops
-
-
-end
diff --git a/tests/Test.thy b/tests/Test.thy
index de65dbd..6f9f996 100644
--- a/tests/Test.thy
+++ b/tests/Test.thy
@@ -1,121 +1,110 @@
-(*  Title:  HoTT/tests/Test.thy
-    Author: Josh Chen
-    Date:   Aug 2018
+(*
+Title:  tests/Test.thy
+Author: Joshua Chen
+Date:   2018
 
-This is an old "test suite" from early implementations of the theory.
-It is not always guaranteed to be up to date, or reflect most recent versions of the theory.
+This is an old test suite from early implementations.
+It is not always guaranteed to be up to date or to reflect most recent versions of the theory.
 *)
 
 theory Test
-  imports "../HoTT"
+imports "../HoTT"
+
 begin
 
 
-text "
-  A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
-  
-  Things that *should* be automated:
-    - Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
-    - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
-"
+text \<open>
+A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
+
+Things that *should* be automated:
+\<^item> Checking that @{term A} is a well-formed type, when writing things like @{prop "x: A"} and @{prop "A: U i"}.
+\<^item> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
+\<close>
 
 declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]]
-  \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
+\<comment> \<open>Turn on trace for unification and the Simplifier, for debugging.\<close>
 
 
 section \<open>\<Prod>-type\<close>
 
 subsection \<open>Typing functions\<close>
 
-text "
-  Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
-"
+text \<open>Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\<close>
 
-proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (routine lems: assms)
+proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A"
+by (routine add: assms)
 
 proposition
   assumes "A : U(i)" and "A \<equiv> B"
   shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
 proof -
   have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp
-  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine lems: assms)
+  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine add: assms)
   ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
 qed
 
 proposition
   assumes "A : U(i)" and "B : U(i)"
   shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A"
-by (routine lems: assms)
-
+by (routine add: assms)
 
 subsection \<open>Function application\<close>
 
-proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (derive lems: assms)
-
-text "Currying:"
+proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a"
+by (derive lems: assms)
 
 lemma
   assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)"
   shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y"
-proof compute
-  show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (routine lems: assms)
-qed fact
+by (derive lems: assms)
 
-lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by derive
+lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b"
+by derive
 
-lemma "\<lbrakk>A: U(i); a : A \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
-proof compute
-  show "\<And>x. \<lbrakk>A: U(i); x: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. f x y: \<Prod>y:B(x). C x y"
-  proof
-    oops
+lemma "\<lbrakk>A: U(i); a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
+proof derive
+oops  \<comment> \<open>Missing some premises.\<close>
 
 lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. \<^bold>\<lambda>y. \<^bold>\<lambda>z. f x y z)`a`b`c \<equiv> f a b c"
-  oops
+proof derive
+oops
 
 
 subsection \<open>Currying functions\<close>
 
 proposition curried_function_formation:
-  fixes A B C
-  assumes
-    "A : U(i)" and
-    "B: A \<longrightarrow> U(i)" and
-    "\<And>x. C(x): B(x) \<longrightarrow> U(i)"
+  assumes "A : U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x. C(x): B(x) \<longrightarrow> U(i)"
   shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U(i)"
-  by (routine lems: assms)
-
+by (routine add: assms)
 
 proposition higher_order_currying_formation:
   assumes
-    "A: U(i)" and
-    "B: A \<longrightarrow> U(i)" and
+    "A: U(i)" and "B: A \<longrightarrow> U(i)" and
     "\<And>x y. y: B(x) \<Longrightarrow> C(x)(y): U(i)" and
     "\<And>x y z. z : C(x)(y) \<Longrightarrow> D(x)(y)(z): U(i)"
   shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z): U(i)"
-  by (routine lems: assms)
-
+by (routine add: assms)
 
 lemma curried_type_judgment:
-  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
+  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
   shows "\<^bold>\<lambda>x y. f x y : \<Prod>x:A. \<Prod>y:B(x). C x y"
-  by (routine lems: assms)
+by (routine add: assms)
 
 
-text "
-  Polymorphic identity function is now trivial due to lambda expression polymorphism.
-  (Was more involved in previous monomorphic incarnations.)
-"
+text \<open>
+Polymorphic identity function is now trivial due to lambda expression polymorphism.
+It was more involved in previous monomorphic incarnations.
+\<close>
 
-definition Id :: "Term" where "Id \<equiv> \<^bold>\<lambda>x. x"
-
-lemma "\<lbrakk>x: A\<rbrakk> \<Longrightarrow> Id`x \<equiv> x"
-unfolding Id_def by (compute, routine)
+lemma "x: A \<Longrightarrow> id`x \<equiv> x"
+by derive
   
 
 section \<open>Natural numbers\<close>
 
-text "Automatic proof methods recognize natural numbers."
+text \<open>Automatic proof methods recognize natural numbers.\<close>
+
+proposition "succ(succ(succ 0)): \<nat>" by routine
 
-proposition "succ(succ(succ 0)): Nat" by routine
 
 end
-- 
cgit v1.2.3