diff options
Diffstat (limited to 'hott/Equivalence.thy')
| -rw-r--r-- | hott/Equivalence.thy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 8007b89..c888714 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -160,7 +160,7 @@ Corollary (def) commute_homotopy': by (rule left_whisker, rewr eq: ap_id, refl) also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x" by (rule commute_homotopy) - finally have "?" by this + finally have "?" by infer thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) qed @@ -240,7 +240,7 @@ Lemma (def) funcomp_is_qinv: have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by compute refl also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact also have ".. ~ id A" by compute fact - finally show "?" by this + finally show "?" by infer qed show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C" @@ -248,7 +248,7 @@ Lemma (def) funcomp_is_qinv: have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by compute refl also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact also have ".. ~ id C" by compute fact - finally show "?" by this + finally show "?" by infer qed qed done @@ -313,10 +313,10 @@ Lemma (def) is_qinv_if_is_biinv: also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric]) also have ".. ~ (id A) \<circ> h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact) also have ".. ~ h" by compute refl - finally have "g ~ h" by this - then have "f \<circ> g ~ f \<circ> h" by (rhtpy, this) + finally have "g ~ h" by infer + then have "f \<circ> g ~ f \<circ> h" by (rhtpy, infer) also note \<open>H2:_\<close> - finally show "f \<circ> g ~ id B" by this + finally show "f \<circ> g ~ id B" by infer qed done done |