From ed41980ed5cee12d7c5eea2e40627e5a390a83f8 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 May 2020 21:31:57 +0200
Subject: minor

---
 hott/Eckmann_Hilton.thy | 10 ++--------
 hott/Identity.thy       |  1 +
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/hott/Eckmann_Hilton.thy b/hott/Eckmann_Hilton.thy
index 09b2c8f..8320256 100644
--- a/hott/Eckmann_Hilton.thy
+++ b/hott/Eckmann_Hilton.thy
@@ -31,8 +31,6 @@ Lemma (derive) left_whisker:
     qed
   done
 
-text \<open>Some notation, or the proofs start getting unwieldy.\<close>
-
 definition right_whisker_i (infix "\<bullet>\<^sub>r\<^bsub>_\<^esub>" 121)
   where [implicit]: "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r \<equiv> right_whisker ? a ? ? ? ? r \<alpha>"
 
@@ -84,9 +82,6 @@ begin
     show "\<alpha>: p = q \<Longrightarrow> .. = q \<bullet> s" by (rule right_whisker)
   qed typechk
 
-  thm horiz_pathcomp_def (* horiz_pathcomp ?\<alpha> ?\<beta> \<equiv> ?\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r \<bullet> (q \<bullet>\<^sub>l\<^bsub>c\<^esub> ?\<beta>) *)
-  thm horiz_pathcomp'_def (* horiz_pathcomp' ?\<alpha> ?\<beta> \<equiv> p \<bullet>\<^sub>l\<^bsub>c\<^esub> ?\<beta> \<bullet> (?\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> s) *)
-
   abbreviation horiz_pathcomp_abbr :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> (infix "\<star>" 121)
     where "\<alpha> \<star> \<beta> \<equiv> horiz_pathcomp \<alpha> \<beta>"
 
@@ -99,7 +94,7 @@ begin
     unfolding horiz_pathcomp_def horiz_pathcomp'_def
     apply (eq \<alpha>, eq \<beta>)
       focus vars p apply (eq p)
-        \<guillemotright> vars _ q by (eq q) (reduce; refl)
+        focus vars _ q by (eq q) (reduce; refl)
       done
     done
 
@@ -118,7 +113,6 @@ Lemma \<Omega>2_alt_def:
 
 section \<open>Eckmann-Hilton\<close>
 
-
 context
 fixes A a
 assumes "A: U i" "a: A"
@@ -183,7 +177,7 @@ begin
     using assms[unfolded \<Omega>2_alt_def]
     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 pathcomp_comp])
+      also have ".. = \<alpha> \<star>' \<beta>" by (rule \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp'[simplified comps])
       also have ".. = \<beta> \<bullet> \<alpha>" by (rule pathcomp_eq_horiz_pathcomp')
       finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" by this (reduce add: \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def)
     qed
diff --git a/hott/Identity.thy b/hott/Identity.thy
index d664fbc..64aea5a 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -145,6 +145,7 @@ Lemma (derive) pathcomp_refl:
 
 definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p"
 definition [implicit]: "lu p \<equiv> refl_pathcomp ? ? ? p"
+
 translations
   "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p"
   "CONST lu p" \<leftharpoondown> "CONST refl_pathcomp A x y p"
-- 
cgit v1.2.3