From fd8ae0b89a703443ef625ca243e6d5ecfa7b2271 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 May 2020 01:18:46 +0200
Subject: Eckmann-Hilton, first pass

---
 hott/Identity.thy | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'hott/Identity.thy')

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