diff options
| author | Josh Chen | 2020-06-01 17:19:27 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-06-01 17:19:27 +0200 |
| commit | 29112d66eb3ecf4139db1da16878d8a817640696 (patch) | |
| tree | 4185f78500dc92603cdbc7cb58f99ae55c79665d /hott | |
| parent | 0834e9922d723b036c0fdc4833d3d920a84ff753 (diff) | |
reorganize and add some material
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Identity.thy | 6 |
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>" |