diff options
author | stuebinm | 2022-06-29 01:28:53 +0200 |
---|---|---|
committer | stuebinm | 2022-06-29 01:28:53 +0200 |
commit | 4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d (patch) | |
tree | 2819976f3fe60d2e9796ec37d2b0736df55daa59 /hott/Equivalence.thy | |
parent | cb4139dc35527bd8c8f9b70753c3d1f552c5f19d (diff) |
this just replaces all instance of `this` with instances of `infer`.
Unfortunately, it looks likes something else also broke, and I have
no idea what it is (but the proof for equiv_if_equal fails).
Sadly this means we can't get to univalence for now …
(but rn I'm too tired to try anything else with it)
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 |