aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2020-06-01 17:19:27 +0200
committerJosh Chen2020-06-01 17:19:27 +0200
commit29112d66eb3ecf4139db1da16878d8a817640696 (patch)
tree4185f78500dc92603cdbc7cb58f99ae55c79665d /hott
parent0834e9922d723b036c0fdc4833d3d920a84ff753 (diff)
reorganize and add some material
Diffstat (limited to '')
-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>"