diff options
| author | Josh Chen | 2020-05-27 21:31:57 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-27 21:31:57 +0200 |
| commit | ed41980ed5cee12d7c5eea2e40627e5a390a83f8 (patch) | |
| tree | 19b5fbf5a7d8bbec09c9f61c9f74c700b69c52b1 /hott | |
| parent | 62c1c8f306bff84b74b3b1c935d0d6722e1251a2 (diff) | |
minor
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Eckmann_Hilton.thy | 10 | ||||
| -rw-r--r-- | 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" |