aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2020-06-03 13:09:45 +0200
committerJosh Chen2020-06-03 13:09:45 +0200
commit515c142828e66dcb1c273e53816ef8b6e1bb3f01 (patch)
tree2b869d03e3df327d84faa77d96a12a31af8a2226 /hott
parente513fc2958133e3a00c06ebcd1214741843acf08 (diff)
rule name
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