diff options
| author | Josh Chen | 2020-05-27 01:18:46 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-27 01:18:46 +0200 |
| commit | fd8ae0b89a703443ef625ca243e6d5ecfa7b2271 (patch) | |
| tree | 2544b556cea59cef647a6e4d8187569a39dbff7a /hott/Identity.thy | |
| parent | b0ba102b783418560f9b7b15239681b11ea4c877 (diff) | |
Eckmann-Hilton, first pass
Diffstat (limited to '')
| -rw-r--r-- | hott/Identity.thy | 16 |
1 files changed, 16 insertions, 0 deletions
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" |