aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to 'hott')
-rw-r--r--hott/Identity.thy6
1 files changed, 3 insertions, 3 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy
index b82c9c2..8675134 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -313,7 +313,7 @@ Lemma (derive) transport_left_inv:
"x: A" "y: A"
"p: x =\<^bsub>A\<^esub> y"
shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)"
- by (eq p) (reduce; intro)
+ by (eq p) (reduce; refl)
Lemma (derive) transport_right_inv:
assumes
@@ -632,8 +632,8 @@ Lemma (derive) eckmann_hilton:
proof -
have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
by (rule pathcomp_eq_horiz_pathcomp)
- also have ".. = \<alpha> \<star>' \<beta>"
- by (rule \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp'[simplified comps])
+ also have [simplified comps]: ".. = \<alpha> \<star>' \<beta>"
+ by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl
also have ".. = \<beta> \<bullet> \<alpha>"
by (rule pathcomp_eq_horiz_pathcomp')
finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"