From b0ba102b783418560f9b7b15239681b11ea4c877 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 26 May 2020 16:50:35 +0200
Subject: new material

---
 hott/Eckmann_Hilton.thy | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 hott/Eckmann_Hilton.thy

(limited to 'hott/Eckmann_Hilton.thy')

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
-- 
cgit v1.2.3