diff options
Diffstat (limited to '')
| -rw-r--r-- | hott/Eckmann_Hilton.thy | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/hott/Eckmann_Hilton.thy b/hott/Eckmann_Hilton.thy new file mode 100644 index 0000000..7355fde --- /dev/null +++ b/hott/Eckmann_Hilton.thy @@ -0,0 +1,21 @@ +theory Eckmann_Hilton +imports Identity + +begin + +Lemma (derive) left_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> + proof - + have "t \<bullet> refl x = t" by (rule pathcomp_refl) + also have ".. = s" by (rule \<open>\<gamma>:_\<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 + + + +end |