From 29112d66eb3ecf4139db1da16878d8a817640696 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 1 Jun 2020 17:19:27 +0200
Subject: reorganize and add some material

---
 hott/Identity.thy | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'hott/Identity.thy')

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>"
-- 
cgit v1.2.3