From 515c142828e66dcb1c273e53816ef8b6e1bb3f01 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 3 Jun 2020 13:09:45 +0200
Subject: rule name

---
 hott/Equivalence.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index aa73ec8..face775 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -387,7 +387,7 @@ Lemma (derive) id_imp_equiv:
       \<^item> prems vars A
         apply (subst transport_comp)
           \<^enum> by (rule U_in_U)
-          \<^enum> by reduce (rule lift_universe)
+          \<^enum> by reduce (rule lift_U)
           \<^enum> by reduce (rule id_biinv)
         done
       done
-- 
cgit v1.2.3