aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--hott/Equivalence.thy2
1 files changed, 1 insertions, 1 deletions
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