aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-29 10:37:46 +0200
committerJosh Chen2020-05-29 10:37:46 +0200
commit2f4e9b941a01a789b17fe208687a27060990e0a7 (patch)
treeb6ee721236107ca8e14cbd95ba7484447a7ec3fa
parent41da54eca527b7c61f13ebcb75a8970bc845bb40 (diff)
clean up Eckmann-Hilton and move to Identity
Diffstat (limited to '')
-rw-r--r--ROOT1
-rw-r--r--hott/Eckmann_Hilton.thy188
-rw-r--r--hott/Equivalence.thy46
-rw-r--r--hott/Identity.thy181
4 files changed, 206 insertions, 210 deletions
diff --git a/ROOT b/ROOT
index 61c5cc4..c960fd7 100644
--- a/ROOT
+++ b/ROOT
@@ -33,4 +33,3 @@ session HoTT in hott = Spartan +
Equivalence
Nat
More_List
- Eckmann_Hilton
diff --git a/hott/Eckmann_Hilton.thy b/hott/Eckmann_Hilton.thy
deleted file mode 100644
index 8320256..0000000
--- a/hott/Eckmann_Hilton.thy
+++ /dev/null
@@ -1,188 +0,0 @@
-theory Eckmann_Hilton
-imports Identity
-
-begin
-
-section \<open>Whiskering and horizontal composition\<close>
-
-Lemma (derive) right_whisker:
- assumes "A: U i" "a: A" "b: A" "c: A"
- shows "\<lbrakk>p: a = b; q: a = b; r: b = c; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> p \<bullet> r = q \<bullet> r"
- apply (eq r)
- focus prems vars x s t \<gamma>
- proof -
- have "t \<bullet> refl x = t" by (rule pathcomp_refl)
- also have ".. = s" by (rule \<open>\<gamma>: t = s\<close>)
- also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric])
- finally show "t \<bullet> refl x = s \<bullet> refl x" by this
- qed
- done
-
-Lemma (derive) left_whisker:
- assumes "A: U i" "a: A" "b: A" "c: A"
- shows "\<lbrakk>p: b = c; q: b = c; r: a = b; \<alpha>: p =\<^bsub>b = c\<^esub> q\<rbrakk> \<Longrightarrow> r \<bullet> p = r \<bullet> q"
- apply (eq r)
- focus prems prms vars x s t \<gamma>
- proof -
- have "refl x \<bullet> t = t" by (rule refl_pathcomp)
- also have ".. = s" by (rule \<open>\<gamma>:_ t = s\<close>)
- also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric])
- finally show "refl x \<bullet> t = refl x \<bullet> s" by this
- qed
- done
-
-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>"
-
-definition left_whisker_i (infix "\<bullet>\<^sub>l\<^bsub>_\<^esub>" 121)
- where [implicit]: "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha> \<equiv> left_whisker ? ? ? c ? ? r \<alpha>"
-
-translations
- "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>"
- "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>"
-
-Lemma whisker_refl [comps]:
- assumes "A: U i" "a: A" "b: A"
- shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow>
- \<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
- unfolding right_whisker_def by reduce
-
-Lemma refl_whisker [comps]:
- assumes "A: U i" "a: A" "b: A"
- shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p = q\<rbrakk> \<Longrightarrow>
- (refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
- unfolding left_whisker_def by reduce
-
-text \<open>Define the conditions under which horizontal composition is well-defined:\<close>
-
-locale horiz_pathcomposable =
-fixes
- i A a b c p q r s
-assumes assums:
- "A: U i" "a: A" "b: A" "c: A"
- "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b"
- "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
-begin
-
- Lemma (derive) horiz_pathcomp:
- notes assums
- shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> ?prf \<alpha> \<beta>: p \<bullet> r = q \<bullet> s"
- proof (rule pathcomp)
- show "\<alpha>: p = q \<Longrightarrow> p \<bullet> r = q \<bullet> r" by (rule right_whisker)
- show "\<beta>: r = s \<Longrightarrow> .. = q \<bullet> s" by (rule left_whisker)
- qed typechk
-
- text \<open>A second horizontal composition:\<close>
-
- Lemma (derive) horiz_pathcomp':
- notes assums
- shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> ?prf \<alpha> \<beta>: p \<bullet> r = q \<bullet> s"
- proof (rule pathcomp)
- show "\<beta>: r = s \<Longrightarrow> p \<bullet> r = p \<bullet> s" by (rule left_whisker)
- show "\<alpha>: p = q \<Longrightarrow> .. = q \<bullet> s" by (rule right_whisker)
- qed typechk
-
- abbreviation horiz_pathcomp_abbr :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> (infix "\<star>" 121)
- where "\<alpha> \<star> \<beta> \<equiv> horiz_pathcomp \<alpha> \<beta>"
-
- abbreviation horiz_pathcomp'_abbr (infix "\<star>''" 121)
- where "\<alpha> \<star>' \<beta> \<equiv> horiz_pathcomp' \<alpha> \<beta>"
-
- Lemma (derive) horiz_pathcomp_eq_horiz_pathcomp':
- notes assums
- shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> \<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
- unfolding horiz_pathcomp_def horiz_pathcomp'_def
- apply (eq \<alpha>, eq \<beta>)
- focus vars p apply (eq p)
- focus vars _ q by (eq q) (reduce; refl)
- done
- done
-
-end
-
-
-section \<open>Loop space\<close>
-
-definition \<Omega> where "\<Omega> A a \<equiv> a =\<^bsub>A\<^esub> a"
-definition \<Omega>2 where "\<Omega>2 A a \<equiv> \<Omega> (\<Omega> A a) (refl a)"
-
-Lemma \<Omega>2_alt_def:
- "\<Omega>2 A a \<equiv> refl a = refl a"
- unfolding \<Omega>2_def \<Omega>_def .
-
-
-section \<open>Eckmann-Hilton\<close>
-
-context
-fixes A a
-assumes "A: U i" "a: A"
-begin
-
- interpretation \<Omega>2:
- horiz_pathcomposable i A a a a "refl a" "refl a" "refl a" "refl a"
- by unfold_locales typechk+
-
- abbreviation horiz_pathcomp (infix "\<star>" 121)
- where "\<alpha> \<star> \<beta> \<equiv> \<Omega>2.horiz_pathcomp \<alpha> \<beta>"
-
- abbreviation horiz_pathcomp' (infix "\<star>''" 121)
- where "\<alpha> \<star>' \<beta> \<equiv> \<Omega>2.horiz_pathcomp' \<alpha> \<beta>"
-
- Lemma (derive) pathcomp_eq_horiz_pathcomp:
- assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
- shows "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
- unfolding \<Omega>2.horiz_pathcomp_def
- using assms[unfolded \<Omega>2_alt_def]
- proof (reduce, rule pathinv)
- \<comment> \<open>Propositional equality rewriting needs to be improved\<close>
- have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
- also have ".. = \<alpha>" by (rule refl_pathcomp)
- finally have eq\<alpha>: "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = \<alpha>" by this
-
- have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
- also have ".. = \<beta>" by (rule refl_pathcomp)
- finally have eq\<beta>: "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = \<beta>" by this
-
- have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))
- = \<alpha> \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))" by (rule right_whisker) (rule eq\<alpha>)
- also have ".. = \<alpha> \<bullet> \<beta>" by (rule left_whisker) (rule eq\<beta>)
- finally show "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))
- = \<alpha> \<bullet> \<beta>" by this
- qed
-
- Lemma (derive) pathcomp_eq_horiz_pathcomp':
- assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
- shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>"
- unfolding \<Omega>2.horiz_pathcomp'_def
- using assms[unfolded \<Omega>2_alt_def]
- proof reduce
- have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
- also have ".. = \<beta>" by (rule refl_pathcomp)
- finally have eq\<beta>: "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = \<beta>" by this
-
- have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
- also have ".. = \<alpha>" by (rule refl_pathcomp)
- finally have eq\<alpha>: "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = \<alpha>" by this
-
- have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))
- = \<beta> \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))" by (rule right_whisker) (rule eq\<beta>)
- also have ".. = \<beta> \<bullet> \<alpha>" by (rule left_whisker) (rule eq\<alpha>)
- finally show "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))
- = \<beta> \<bullet> \<alpha>" by this
- qed
-
- Lemma (derive) eckmann_hilton:
- assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
- shows "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
- 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 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
-
-end
-
-
-end
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 9e7b83a..9c86a95 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -138,6 +138,11 @@ Lemma homotopy_funcomp_right:
apply (rule ap, assumption)
done
+method id_htpy = (rule homotopy_id_left)
+method htpy_id = (rule homotopy_id_right)
+method htpy_o = (rule homotopy_funcomp_left)
+method o_htpy = (rule homotopy_funcomp_right)
+
section \<open>Quasi-inverse and bi-invertibility\<close>
@@ -187,15 +192,20 @@ Lemma (derive) funcomp_qinv:
"f: A \<rightarrow> B" "g: B \<rightarrow> C"
shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)"
apply (intros, unfold qinv_def, elims)
- focus
- prems prms
- vars _ _ finv _ ginv _ HfA HfB HgB HgC
-
- apply intro
- apply (rule funcompI[where ?f=ginv and ?g=finv])
-
- text \<open>Now a whole bunch of rewrites and we're done.\<close>
-oops
+ focus prems vars _ _ finv _ ginv
+ apply (intro, rule funcompI[where ?f=ginv and ?g=finv])
+ proof (reduce, intro)
+ have "finv \<circ> ginv \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl
+ also have ".. ~ finv \<circ> id B \<circ> f" by (o_htpy, htpy_o) fact
+ also have ".. ~ id A" by reduce fact
+ finally show "finv \<circ> ginv \<circ> g \<circ> f ~ id A" by this
+
+ have "g \<circ> f \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl
+ also have ".. ~ g \<circ> id B \<circ> ginv" by (o_htpy, htpy_o) fact
+ also have ".. ~ id C" by reduce fact
+ finally show "g \<circ> f \<circ> finv \<circ> ginv ~ id C" by this
+ qed
+ done
subsection \<open>Bi-invertible maps\<close>
@@ -246,10 +256,10 @@ Lemma (derive) biinv_imp_qinv:
\<close>
unfolding qinv_def
apply intro
- \<guillemotright> by (rule \<open>g: _\<close>)
+ \<guillemotright> by (fact \<open>g: _\<close>)
\<guillemotright> apply intro
text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close>
- apply (rule \<open>H1: _\<close>)
+ apply (fact \<open>H1: _\<close>)
text \<open>
It remains to prove \<^prop>\<open>?H2: f \<circ> g ~ id B\<close>. First show that \<open>g ~ h\<close>,
@@ -258,19 +268,13 @@ Lemma (derive) biinv_imp_qinv:
\<close>
proof -
have "g ~ g \<circ> (id B)" by reduce refl
- also have ".. ~ g \<circ> f \<circ> h"
- by (rule homotopy_funcomp_right) (rule \<open>H2:_\<close>[symmetric])
- also have ".. ~ (id A) \<circ> h"
- by (subst funcomp_assoc[symmetric])
- (rule homotopy_funcomp_left, rule \<open>H1:_\<close>)
+ also have ".. ~ g \<circ> f \<circ> h" by o_htpy (rule \<open>H2:_\<close>[symmetric])
+ also have ".. ~ (id A) \<circ> h" by (subst funcomp_assoc[symmetric]) (htpy_o, fact)
also have ".. ~ h" by reduce refl
finally have "g ~ h" by this
-
then have "f \<circ> g ~ f \<circ> h" by (rule homotopy_funcomp_right)
-
- with \<open>H2:_\<close>
- show "f \<circ> g ~ id B"
- by (rule homotopy_trans) (assumption+, typechk)
+ also note \<open>H2:_\<close>
+ finally show "f \<circ> g ~ id B" by this
qed
done
done
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 64aea5a..571617a 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -460,4 +460,185 @@ Lemma (derive) apd_ap:
by (eq p) (reduce; intro)
+section \<open>Whiskering\<close>
+
+Lemma (derive) right_whisker:
+ assumes "A: U i" "a: A" "b: A" "c: A"
+ shows "\<lbrakk>p: a = b; q: a = b; r: b = c; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> p \<bullet> r = q \<bullet> r"
+ apply (eq r)
+ focus prems vars x s t
+ proof -
+ have "t \<bullet> refl x = t" by (rule pathcomp_refl)
+ also have ".. = s" by fact
+ also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric])
+ finally show "t \<bullet> refl x = s \<bullet> refl x" by this
+ qed
+ done
+
+Lemma (derive) left_whisker:
+ assumes "A: U i" "a: A" "b: A" "c: A"
+ shows "\<lbrakk>p: b = c; q: b = c; r: a = b; \<alpha>: p =\<^bsub>b = c\<^esub> q\<rbrakk> \<Longrightarrow> r \<bullet> p = r \<bullet> q"
+ apply (eq r)
+ focus prems prms vars x s t
+ proof -
+ have "refl x \<bullet> t = t" by (rule refl_pathcomp)
+ also have ".. = s" by fact
+ also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric])
+ finally show "refl x \<bullet> t = refl x \<bullet> s" by this
+ qed
+ done
+
+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>"
+
+definition left_whisker_i (infix "\<bullet>\<^sub>l\<^bsub>_\<^esub>" 121)
+ where [implicit]: "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha> \<equiv> left_whisker ? ? ? c ? ? r \<alpha>"
+
+translations
+ "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>"
+ "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>"
+
+Lemma whisker_refl [comps]:
+ assumes "A: U i" "a: A" "b: A"
+ shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow>
+ \<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
+ unfolding right_whisker_def by reduce
+
+Lemma refl_whisker [comps]:
+ assumes "A: U i" "a: A" "b: A"
+ shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p = q\<rbrakk> \<Longrightarrow>
+ (refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
+ unfolding left_whisker_def by reduce
+
+method left_whisker = (rule left_whisker)
+method right_whisker = (rule right_whisker)
+
+
+section \<open>Horizontal path-composition\<close>
+
+text \<open>Conditions under which horizontal path-composition is defined.\<close>
+locale horiz_pathcomposable =
+fixes
+ i A a b c p q r s
+assumes assums:
+ "A: U i" "a: A" "b: A" "c: A"
+ "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b"
+ "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
+begin
+
+Lemma (derive) horiz_pathcomp:
+ notes assums
+ shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> ?prf \<alpha> \<beta>: p \<bullet> r = q \<bullet> s"
+proof (rule pathcomp)
+ show "\<alpha>: p = q \<Longrightarrow> p \<bullet> r = q \<bullet> r" by right_whisker
+ show "\<beta>: r = s \<Longrightarrow> .. = q \<bullet> s" by left_whisker
+qed typechk
+
+text \<open>A second horizontal composition:\<close>
+
+Lemma (derive) horiz_pathcomp':
+ notes assums
+ shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> ?prf \<alpha> \<beta>: p \<bullet> r = q \<bullet> s"
+proof (rule pathcomp)
+ show "\<beta>: r = s \<Longrightarrow> p \<bullet> r = p \<bullet> s" by left_whisker
+ show "\<alpha>: p = q \<Longrightarrow> .. = q \<bullet> s" by right_whisker
+qed typechk
+
+notation horiz_pathcomp (infix "\<star>" 121)
+notation horiz_pathcomp' (infix "\<star>''" 121)
+
+Lemma (derive) horiz_pathcomp_eq_horiz_pathcomp':
+ notes assums
+ shows "\<lbrakk>\<alpha>: p = q; \<beta>: r = s\<rbrakk> \<Longrightarrow> \<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
+ unfolding horiz_pathcomp_def horiz_pathcomp'_def
+ apply (eq \<alpha>, eq \<beta>)
+ focus vars p apply (eq p)
+ focus vars _ q by (eq q) (reduce; refl)
+ done
+ done
+
+end
+
+
+section \<open>Loop space\<close>
+
+definition \<Omega> where "\<Omega> A a \<equiv> a =\<^bsub>A\<^esub> a"
+definition \<Omega>2 where "\<Omega>2 A a \<equiv> \<Omega> (\<Omega> A a) (refl a)"
+
+Lemma \<Omega>2_alt_def:
+ "\<Omega>2 A a \<equiv> refl a = refl a"
+ unfolding \<Omega>2_def \<Omega>_def .
+
+
+section \<open>Eckmann-Hilton\<close>
+
+context fixes i A a assumes "A: U i" "a: A"
+begin
+
+interpretation \<Omega>2:
+ horiz_pathcomposable i A a a a "refl a" "refl a" "refl a" "refl a"
+ by unfold_locales typechk+
+
+notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121)
+notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121)
+
+Lemma (derive) pathcomp_eq_horiz_pathcomp:
+ assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
+ shows "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
+ unfolding \<Omega>2.horiz_pathcomp_def
+ using assms[unfolded \<Omega>2_alt_def]
+ proof (reduce, rule pathinv)
+ \<comment> \<open>Propositional equality rewriting needs to be improved\<close>
+ have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
+ also have ".. = \<alpha>" by (rule refl_pathcomp)
+ finally have eq\<alpha>: "{} = \<alpha>" by this
+
+ have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
+ also have ".. = \<beta>" by (rule refl_pathcomp)
+ finally have eq\<beta>: "{} = \<beta>" by this
+
+ have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))
+ = \<alpha> \<bullet> {}" by right_whisker (rule eq\<alpha>)
+ also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (rule eq\<beta>)
+ finally show "{} = \<alpha> \<bullet> \<beta>" by this
+ qed
+
+Lemma (derive) pathcomp_eq_horiz_pathcomp':
+ assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
+ shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>"
+ unfolding \<Omega>2.horiz_pathcomp'_def
+ using assms[unfolded \<Omega>2_alt_def]
+ proof reduce
+ have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
+ also have ".. = \<beta>" by (rule refl_pathcomp)
+ finally have eq\<beta>: "{} = \<beta>" by this
+
+ have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
+ also have ".. = \<alpha>" by (rule refl_pathcomp)
+ finally have eq\<alpha>: "{} = \<alpha>" by this
+
+ have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))
+ = \<beta> \<bullet> {}" by right_whisker (rule eq\<beta>)
+ also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (rule eq\<alpha>)
+ finally show "{} = \<beta> \<bullet> \<alpha>" by this
+ qed
+
+Lemma (derive) eckmann_hilton:
+ assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
+ shows "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
+ 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 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
+
+end
+
+
end