From 55c148073df8de5f0cf4c45db23d2e3da7f4f093 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 20 Sep 2018 21:35:51 +0200
Subject: Derive can prove pathcomp_comp. Fix typo.

---
 Equality.thy  | 16 +---------------
 HoTT_Base.thy |  2 +-
 2 files changed, 2 insertions(+), 16 deletions(-)

diff --git a/Equality.thy b/Equality.thy
index 05ccbff..851c569 100644
--- a/Equality.thy
+++ b/Equality.thy
@@ -51,21 +51,7 @@ by (routine add: assms pathcomp_type)
 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)
+unfolding pathcomp_def by (derive lems: assms)
 
 declare
   pathcomp_type [intro]
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 0b460d9..9e8fee7 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -53,7 +53,7 @@ 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.
 
-@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}.
+@{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
 \<close>
 
 
-- 
cgit v1.2.3