diff options
Diffstat (limited to 'hott/Identity.thy')
| -rw-r--r-- | hott/Identity.thy | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index ce0e0ec..6c044b4 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -203,6 +203,7 @@ Lemma (def) ap: shows "f x = f y" by (eq p) intro + definition ap_i ("_[_]" [1000, 0]) where [implicit]: "ap_i f p \<equiv> ap {} {} {} {} f p" @@ -304,7 +305,7 @@ Lemma (def) pathcomp_cancel_left: by (rewr eq: pathcomp_assoc, rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl - finally show "?" by this + finally show "?" by infer qed Lemma (def) pathcomp_cancel_right: @@ -323,7 +324,7 @@ Lemma (def) pathcomp_cancel_right: rewr eq: pathcomp_assoc[symmetric], rewr eq: pathcomp_inv, rewr eq: pathcomp_refl) refl - finally show "?" by this + finally show "?" by infer qed method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] @@ -488,7 +489,7 @@ Lemma (def) right_whisker: have "s \<bullet> refl x = s" by (rule pathcomp_refl) also have ".. = t" by fact also have ".. = t \<bullet> refl x" by (rule pathcomp_refl[symmetric]) - finally show "?" by this + finally show "?" by infer qed done @@ -502,7 +503,7 @@ Lemma (def) left_whisker: have "refl x \<bullet> s = s" by (rule refl_pathcomp) also have ".. = t" by fact also have ".. = refl x \<bullet> t" by (rule refl_pathcomp[symmetric]) - finally show "?" by this + finally show "?" by infer qed done @@ -608,17 +609,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp: have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl) also have ".. = \<alpha>" by (rule refl_pathcomp) - finally have eq\<alpha>: "? = \<alpha>" by this + finally have eq\<alpha>: "? = \<alpha>" by infer have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl) also have ".. = \<beta>" by (rule refl_pathcomp) - finally have eq\<beta>: "? = \<beta>" by this + finally have eq\<beta>: "? = \<beta>" by infer have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a)) = \<alpha> \<bullet> ?" by right_whisker (fact eq\<alpha>) also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (fact eq\<beta>) - finally show "? = \<alpha> \<bullet> \<beta>" by this + finally show "? = \<alpha> \<bullet> \<beta>" by infer qed Lemma (def) pathcomp_eq_horiz_pathcomp': @@ -630,17 +631,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl) also have ".. = \<beta>" by (rule refl_pathcomp) - finally have eq\<beta>: "? = \<beta>" by this + finally have eq\<beta>: "? = \<beta>" by infer have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl) also have ".. = \<alpha>" by (rule refl_pathcomp) - finally have eq\<alpha>: "? = \<alpha>" by this + finally have eq\<alpha>: "? = \<alpha>" by infer have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a)) = \<beta> \<bullet> ?" by right_whisker (fact eq\<beta>) also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (fact eq\<alpha>) - finally show "? = \<beta> \<bullet> \<alpha>" by this + finally show "? = \<beta> \<bullet> \<alpha>" by infer qed Lemma (def) eckmann_hilton: @@ -657,7 +658,7 @@ Lemma (def) eckmann_hilton: also have ".. = \<beta> \<bullet> \<alpha>" by (rule pathcomp_eq_horiz_pathcomp') finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" - by this + by infer qed end |