aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to 'hott')
-rw-r--r--hott/Eckmann_Hilton.thy179
-rw-r--r--hott/Identity.thy16
2 files changed, 192 insertions, 3 deletions
diff --git a/hott/Eckmann_Hilton.thy b/hott/Eckmann_Hilton.thy
index 7355fde..09b2c8f 100644
--- a/hott/Eckmann_Hilton.thy
+++ b/hott/Eckmann_Hilton.thy
@@ -3,19 +3,192 @@ imports Identity
begin
-Lemma (derive) left_whisker:
+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 prms vars x s t \<gamma>
+ 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>:_\<close>)
+ 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
+
+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>"
+
+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
+
+ 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>"
+
+ 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)
+ \<guillemotright> 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 pathcomp_comp])
+ 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/Identity.thy b/hott/Identity.thy
index d60f4c2..d664fbc 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -143,6 +143,22 @@ Lemma (derive) pathcomp_refl:
apply (reduce; intros)
done
+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"
+
+Lemma lu_refl [comps]:
+ assumes "A: U i" "x: A"
+ shows "lu (refl x) \<equiv> refl (refl x)"
+ unfolding refl_pathcomp_def by reduce
+
+Lemma ru_refl [comps]:
+ assumes "A: U i" "x: A"
+ shows "ru (refl x) \<equiv> refl (refl x)"
+ unfolding pathcomp_refl_def by reduce
+
Lemma (derive) inv_pathcomp:
assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
shows "p\<inverse> \<bullet> p = refl y"