diff options
author | Josh Chen | 2020-05-26 16:50:35 +0200 |
---|---|---|
committer | Josh Chen | 2020-05-26 16:50:35 +0200 |
commit | b0ba102b783418560f9b7b15239681b11ea4c877 (patch) | |
tree | 0158979a77c146f254eab072b300b0fb2579f1a4 /hott/Eckmann_Hilton.thy | |
parent | 028f43a0737128024742234f3ee95b24986d6403 (diff) |
new material
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 |