From 06f38e1bad882ec85cbfd89b74feef380c8bbd69 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 28 Jun 2021 13:34:31 +0100 Subject: begin refactoring Equivalence --- hott/Equivalence2.thy | 458 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 458 insertions(+) create mode 100644 hott/Equivalence2.thy diff --git a/hott/Equivalence2.thy b/hott/Equivalence2.thy new file mode 100644 index 0000000..e6f9ca9 --- /dev/null +++ b/hott/Equivalence2.thy @@ -0,0 +1,458 @@ +(*This is a rewrite of Equivalence.thy using the new Definition mechanism to abstract + sections and retractions.*) + +theory Equivalence2 +imports Identity + +begin + +section \Homotopy\ + +Definition homotopy: ":= \x: A. f x = g x" + where "A: U i" "\x. x: A \ B x: U i" "f: \x: A. B x" "g: \x: A. B x" + by typechk + +definition homotopy_i (infix "~" 100) + where [implicit]: "f ~ g \ homotopy {} {} f g" + +translations "f ~ g" \ "CONST homotopy A B f g" + +Lemma apply_homotopy: + assumes + "A: U i" "\x. x: A \ B x: U i" + "f: \x: A. B x" "g: \x: A. B x" + "H: f ~ g" + "x: A" + shows "H x: f x = g x" + using \H:_\ unfolding homotopy_def + by typechk + +method htpy for H::o = rule apply_homotopy[where ?H=H] + +Lemma (def) homotopy_refl [refl]: + assumes + "A: U i" + "f: \x: A. B x" + shows "f ~ f" + unfolding homotopy_def + by intros fact + +Lemma (def) hsym: + assumes + "A: U i" + "\x. x: A \ B x: U i" + "f: \x: A. B x" + "g: \x: A. B x" + "H: f ~ g" + shows "g ~ f" + unfolding homotopy_def + proof intro + fix x assuming "x: A" then have "f x = g x" + by (htpy H) + thus "g x = f x" + by (rule pathinv) fact + qed + +Lemma (def) htrans: + assumes + "A: U i" + "\x. x: A \ B x: U i" + "f: \x: A. B x" + "g: \x: A. B x" + "h: \x: A. B x" + "H1: f ~ g" + "H2: g ~ h" + shows "f ~ h" + unfolding homotopy_def + proof intro + fix x assuming "x: A" + have *: "f x = g x" "g x = h x" + by (htpy H1, htpy H2) + show "f x = h x" + by (rule pathcomp; (rule *)?) typechk + qed + +section \Rewriting homotopies\ + +calc "f ~ g" rhs g + +lemmas + homotopy_sym [sym] = hsym[rotated 4] and + homotopy_trans [trans] = htrans[rotated 5] + +Lemma id_funcomp_htpy: + assumes "A: U i" "B: U i" "f: A \ B" + shows "homotopy_refl A f: (id B) \ f ~ f" + by compute + +Lemma funcomp_id_htpy: + assumes "A: U i" "B: U i" "f: A \ B" + shows "homotopy_refl A f: f \ (id A) ~ f" + by compute + +Lemma funcomp_left_htpy: + assumes + "A: U i" "B: U i" + "\x. x: B \ C x: U i" + "f: A \ B" + "g: \x: B. C x" + "g': \x: B. C x" + "H: g ~ g'" + shows "(g \ f) ~ (g' \ f)" + unfolding homotopy_def + apply (intro, compute) + apply (htpy H) + done + +Lemma funcomp_right_htpy: + assumes + "A: U i" "B: U i" "C: U i" + "f: A \ B" + "f': A \ B" + "g: B \ C" + "H: f ~ f'" + shows "(g \ f) ~ (g \ f')" + unfolding homotopy_def + proof (intro, compute) + fix x assuming "x: A" + have *: "f x = f' x" + by (htpy H) + show "g (f x) = g (f' x)" + by (rewr eq: *) refl + qed + +method lhtpy = rule funcomp_left_htpy[rotated 6] +method rhtpy = rule funcomp_right_htpy[rotated 6] + +Lemma (def) commute_homotopy: + assumes + "A: U i" "B: U i" + "x: A" "y: A" + "p: x = y" + "f: A \ B" "g: A \ B" + "H: f ~ g" + shows "(H x) \ g[p] = f[p] \ (H y)" + using \H:_\ + unfolding homotopy_def + apply (eq p, compute) + apply (rewr eq: pathcomp_refl, rewr eq: refl_pathcomp) + by refl + +Corollary (def) commute_homotopy': + assumes + "A: U i" + "x: A" + "f: A \ A" + "H: f ~ (id A)" + shows "H (f x) = f [H x]" + proof - + (*FUTURE: Because we don't have very good normalization integrated into + things yet, we need to manually unfold the type of H.*) + from \H: f ~ id A\ have [type]: "H: \x: A. f x = x" + by (compute add: homotopy_def) + + have "H (f x) \ H x = H (f x) \ (id A)[H x]" + by (rule left_whisker, rewr eq: ap_id, refl) + also have [simplified id_comp]: "H (f x) \ (id A)[H x] = f[H x] \ H x" + by (rule commute_homotopy) + finally have "?" by this + + thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) + qed + + +section \Quasi-inverse and bi-invertibility\ + +subsection \Sections and retractions\ + +Definition retraction: ":= g \ f ~ id A" + where "A: U i" "B: U i" "f: A \ B" "g: B \ A" + by typechk + +Definition "section": ":= f \ g ~ id B" + where "A: U i" "B: U i" "f: A \ B" "g: B \ A" + by typechk + +definition retraction_i ("retraction") + where [implicit]: "retraction f g \ Equivalence.retraction {} f g" + +definition section_i ("section") + where [implicit]: "section f g \ Equivalence.section {} f g" + +Lemma (def) id_is_retraction: + assumes "A: U i" + shows "retraction (id A) (id A)" + unfolding retraction_def + by compute refl + +Lemma (def) id_is_section: + assumes "A: U i" + shows "section (id A) (id A)" + unfolding section_def + by compute refl + +Lemma + assumes "A: U i" "B: U i" "f: A \ B" "g: B \ A" + shows + section_of_retraction: "h: retraction f g \ h: section g f" and + retraction_of_section: "h: section f g \ h: retraction g f" + unfolding section_def retraction_def . + +subsection \Quasi-inverses\ + +Definition is_qinv: ":= \g: B \ A. section f g \ retraction f g" + where "A: U i" "B: U i" "f: A \ B" + by typechk + +definition is_qinv_i ("is'_qinv") + where [implicit]: "is_qinv f \ Equivalence.is_qinv {} {} f" + +no_translations "is_qinv f" \ "CONST Equivalence.is_qinv A B f" + +Lemma (def) id_is_qinv: + assumes "A: U i" + shows "is_qinv (id A)" + unfolding is_qinv_def + proof intro + show "id A: A \ A" by typechk + qed (intro, rule id_is_section, rule id_is_retraction) + +Lemma is_qinvI: + assumes + "A: U i" "B: U i" "f: A \ B" + "g: B \ A" + "H1: section f g" + "H2: retraction f g" + shows "is_qinv f" + unfolding is_qinv_def + by (intro, fact, intro; fact) + +Lemma is_qinv_components [type]: + assumes "A: U i" "B: U i" "f: A \ B" "fq: is_qinv f" + shows + qinv_of_is_qinv: "fst fq: B \ A" and + sec_of_is_qinv: "p\<^sub>2\<^sub>1 fq: section f (fst fq)" and + ret_of_is_qinv: "p\<^sub>2\<^sub>2 fq: retraction f (fst fq)" + using assms unfolding is_qinv_def + by typechk+ + +Lemma (def) qinv_is_qinv: + assumes "A: U i" "B: U i" "f: A \ B" "pf: is_qinv f" + shows "is_qinv (fst pf)" + apply (rule is_qinvI) + \<^item> by fact + \<^item> by (rule section_of_retraction) (rule ret_of_is_qinv) + \<^item> by (rule retraction_of_section) (rule sec_of_is_qinv) + done + +(*Note the issues with definitional folding/unfolding in the following proof.*) +Lemma (def) funcomp_of_qinv: + assumes + "A: U i" "B: U i" "C: U i" + "f: A \ B" "g: B \ C" + shows "is_qinv f \ is_qinv g \ is_qinv (g \ f)" + apply intros + apply (rule is_qinvI) + \<^item> vars fq gq + proof - + show "fst fq \ fst gq: C \ A" by typechk + qed + \<^item> vars fq gq + proof - + have "(g \ f) \ fst fq \ fst gq ~ g \ (f \ fst fq) \ fst gq" by (compute, refl) + also have ".. ~ g \ id B \ fst gq" by (rhtpy, lhtpy, fold section_def, rule sec_of_is_qinv) + also have ".. ~ id C" by (compute, unfold section_def, rule sec_of_is_qinv[unfolded section_def]) + finally have [folded section_def]: "?" by this + then show "?" . + qed + \<^item> vars fq gq + proof - + +(*An alternative proof to the above starts with + apply intros + unfolding is_qinv_def apply elims + focus vars _ _ finv ginv +*) + +subsection \Bi-invertible maps\ + +definition "is_biinv A B f \ + (\g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A)) + \ (\g: B \ A. homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B))" + +Lemma is_biinv_type [type]: + assumes "A: U i" "B: U i" "f: A \ B" + shows "is_biinv A B f: U i" + unfolding is_biinv_def by typechk + +definition is_biinv_i ("is'_biinv") + where [implicit]: "is_biinv f \ Equivalence.is_biinv {} {} f" + +translations "is_biinv f" \ "CONST Equivalence.is_biinv A B f" + +Lemma is_biinvI: + assumes + "A: U i" "B: U i" "f: A \ B" + "g: B \ A" "h: B \ A" + "H1: g \ f ~ id A" "H2: f \ h ~ id B" + shows "is_biinv f" + unfolding is_biinv_def + proof intro + show ": \g: B \ A. g \ f ~ id A" by typechk + show ": \g: B \ A. f \ g ~ id B" by typechk + qed + +Lemma is_biinv_components [type]: + assumes "A: U i" "B: U i" "f: A \ B" "pf: is_biinv f" + shows + section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \ A" and + retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \ A" and + ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \ f ~ id A" and + sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \ p\<^sub>2\<^sub>1 pf ~ id B" + using assms unfolding is_biinv_def + by typechk+ + +Lemma (def) is_biinv_if_is_qinv: + assumes "A: U i" "B: U i" "f: A \ B" + shows "is_qinv f \ is_biinv f" + apply intros + unfolding is_qinv_def is_biinv_def + by (rule distribute_Sig) + +Lemma (def) is_qinv_if_is_biinv: + assumes "A: U i" "B: U i" "f: A \ B" + shows "is_biinv f \ is_qinv f" + apply intro + unfolding is_biinv_def apply elims + focus vars _ _ _ g H1 h H2 + apply (rule is_qinvI) + \<^item> by (fact \g: _\) + \<^item> by (fact \H1: _\) + \<^item> proof - + have "g ~ g \ (id B)" by compute refl + also have ".. ~ g \ f \ h" by rhtpy (rule \H2:_\[symmetric]) + also have ".. ~ (id A) \ h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact) + also have ".. ~ h" by compute refl + finally have "g ~ h" by this + then have "f \ g ~ f \ h" by (rhtpy, this) + also note \H2:_\ + finally show "f \ g ~ id B" by this + qed + done + done + +Lemma (def) id_is_biinv: + "A: U i \ is_biinv (id A)" + by (rule is_biinv_if_is_qinv) (rule id_is_qinv) + +Lemma (def) funcomp_is_biinv: + assumes + "A: U i" "B: U i" "C: U i" + "f: A \ B" "g: B \ C" + shows "is_biinv f \ is_biinv g \ is_biinv (g \ f)" + apply intros + focus vars pf pg + by (rule is_biinv_if_is_qinv) + (rule funcomp_is_qinv; rule is_qinv_if_is_biinv, fact) + done + + +section \Equivalence\ + +text \ + Following the HoTT book, we first define equivalence in terms of + bi-invertibility. +\ + +definition equivalence (infix "\" 110) + where "A \ B \ \f: A \ B. Equivalence.is_biinv A B f" + +Lemma equivalence_type [type]: + assumes "A: U i" "B: U i" + shows "A \ B: U i" + unfolding equivalence_def by typechk + +Lemma (def) equivalence_refl: + assumes "A: U i" + shows "A \ A" + unfolding equivalence_def + proof intro + show "is_biinv (id A)" by (rule is_biinv_if_is_qinv) (rule id_is_qinv) + qed typechk + +Lemma (def) equivalence_symmetric: + assumes "A: U i" "B: U i" + shows "A \ B \ B \ A" + apply intros + unfolding equivalence_def + apply elim + apply (dest (4) is_qinv_if_is_biinv) + apply intro + \<^item> by (rule qinv_of_is_qinv) facts + \<^item> by (rule is_biinv_if_is_qinv) (rule qinv_is_qinv) + done + +Lemma (def) equivalence_transitive: + assumes "A: U i" "B: U i" "C: U i" + shows "A \ B \ B \ C \ A \ C" + proof intros + fix AB BC assume *: "AB: A \ B" "BC: B \ C" + then have + "fst AB: A \ B" and 1: "snd AB: is_biinv (fst AB)" + "fst BC: B \ C" and 2: "snd BC: is_biinv (fst BC)" + unfolding equivalence_def by typechk+ + then have "fst BC \ fst AB: A \ C" by typechk + moreover have "is_biinv (fst BC \ fst AB)" + using * unfolding equivalence_def by (rule funcomp_is_biinv 1 2) facts + ultimately show "A \ C" + unfolding equivalence_def by intro facts + qed + +text \ + Equal types are equivalent. We give two proofs: the first by induction, and + the second by following the HoTT book and showing that transport is an + equivalence. +\ + +Lemma + assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" + shows "A \ B" + by (eq p) (rule equivalence_refl) + +text \ + The following proof is wordy because (1) typechecker normalization is still + rudimentary, and (2) we don't yet have universe level inference. +\ + +Lemma (def) equiv_if_equal: + assumes + "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" + shows ": A \ B" + unfolding equivalence_def + apply intro defer + \<^item> apply (eq p) + \<^enum> vars A B + apply (comp at A in "A \ B" id_comp[symmetric]) + using [[solve_side_conds=1]] + apply (comp at B in "_ \ B" id_comp[symmetric]) + apply (rule transport, rule Ui_in_USi) + by (rule lift_universe_codomain, rule Ui_in_USi) + \<^enum> vars A + using [[solve_side_conds=1]] + apply (comp transport_comp) + \ by (rule Ui_in_USi) + \ by compute (rule U_lift) + \ by compute (rule id_is_biinv) + done + done + + \<^item> \ \Similar proof as in the first subgoal above\ + apply (comp at A in "A \ B" id_comp[symmetric]) + using [[solve_side_conds=1]] + apply (comp at B in "_ \ B" id_comp[symmetric]) + apply (rule transport, rule Ui_in_USi) + by (rule lift_universe_codomain, rule Ui_in_USi) + done + + +end -- cgit v1.2.3