diff options
| -rw-r--r-- | ROOT | 1 | ||||
| -rw-r--r-- | hott/Eckmann_Hilton.thy | 188 | ||||
| -rw-r--r-- | hott/Equivalence.thy | 46 | ||||
| -rw-r--r-- | hott/Identity.thy | 181 |
4 files changed, 206 insertions, 210 deletions
@@ -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 |