1 files changed, 181 insertions, 0 deletions
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