aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--hott/Equivalence2.thy458
1 files changed, 458 insertions, 0 deletions
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 \<open>Homotopy\<close>
+
+Definition homotopy: ":= \<Prod>x: A. f x = g x"
+ where "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+ by typechk
+
+definition homotopy_i (infix "~" 100)
+ where [implicit]: "f ~ g \<equiv> homotopy {} {} f g"
+
+translations "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
+
+Lemma apply_homotopy:
+ assumes
+ "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+ "H: f ~ g"
+ "x: A"
+ shows "H x: f x = g x"
+ using \<open>H:_\<close> 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: \<Prod>x: A. B x"
+ shows "f ~ f"
+ unfolding homotopy_def
+ by intros fact
+
+Lemma (def) hsym:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "f: \<Prod>x: A. B x"
+ "g: \<Prod>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"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "f: \<Prod>x: A. B x"
+ "g: \<Prod>x: A. B x"
+ "h: \<Prod>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 \<open>Rewriting homotopies\<close>
+
+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 \<rightarrow> B"
+ shows "homotopy_refl A f: (id B) \<circ> f ~ f"
+ by compute
+
+Lemma funcomp_id_htpy:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "homotopy_refl A f: f \<circ> (id A) ~ f"
+ by compute
+
+Lemma funcomp_left_htpy:
+ assumes
+ "A: U i" "B: U i"
+ "\<And>x. x: B \<Longrightarrow> C x: U i"
+ "f: A \<rightarrow> B"
+ "g: \<Prod>x: B. C x"
+ "g': \<Prod>x: B. C x"
+ "H: g ~ g'"
+ shows "(g \<circ> f) ~ (g' \<circ> 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 \<rightarrow> B"
+ "f': A \<rightarrow> B"
+ "g: B \<rightarrow> C"
+ "H: f ~ f'"
+ shows "(g \<circ> f) ~ (g \<circ> 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 \<rightarrow> B" "g: A \<rightarrow> B"
+ "H: f ~ g"
+ shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
+ using \<open>H:_\<close>
+ 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 \<rightarrow> 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 \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
+ by (compute add: homotopy_def)
+
+ have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
+ 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
+
+ thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+)
+ qed
+
+
+section \<open>Quasi-inverse and bi-invertibility\<close>
+
+subsection \<open>Sections and retractions\<close>
+
+Definition retraction: ":= g \<circ> f ~ id A"
+ where "A: U i" "B: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> A"
+ by typechk
+
+Definition "section": ":= f \<circ> g ~ id B"
+ where "A: U i" "B: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> A"
+ by typechk
+
+definition retraction_i ("retraction")
+ where [implicit]: "retraction f g \<equiv> Equivalence.retraction {} f g"
+
+definition section_i ("section")
+ where [implicit]: "section f g \<equiv> 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 \<rightarrow> B" "g: B \<rightarrow> A"
+ shows
+ section_of_retraction: "h: retraction f g \<Longrightarrow> h: section g f" and
+ retraction_of_section: "h: section f g \<Longrightarrow> h: retraction g f"
+ unfolding section_def retraction_def .
+
+subsection \<open>Quasi-inverses\<close>
+
+Definition is_qinv: ":= \<Sum>g: B \<rightarrow> A. section f g \<times> retraction f g"
+ where "A: U i" "B: U i" "f: A \<rightarrow> B"
+ by typechk
+
+definition is_qinv_i ("is'_qinv")
+ where [implicit]: "is_qinv f \<equiv> Equivalence.is_qinv {} {} f"
+
+no_translations "is_qinv f" \<leftharpoondown> "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 \<rightarrow> 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 \<rightarrow> B"
+ "g: B \<rightarrow> 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 \<rightarrow> B" "fq: is_qinv f"
+ shows
+ qinv_of_is_qinv: "fst fq: B \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> B" "g: B \<rightarrow> C"
+ shows "is_qinv f \<rightarrow> is_qinv g \<rightarrow> is_qinv (g \<circ> f)"
+ apply intros
+ apply (rule is_qinvI)
+ \<^item> vars fq gq
+ proof -
+ show "fst fq \<circ> fst gq: C \<rightarrow> A" by typechk
+ qed
+ \<^item> vars fq gq
+ proof -
+ have "(g \<circ> f) \<circ> fst fq \<circ> fst gq ~ g \<circ> (f \<circ> fst fq) \<circ> fst gq" by (compute, refl)
+ also have ".. ~ g \<circ> id B \<circ> 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 \<open>Bi-invertible maps\<close>
+
+definition "is_biinv A B f \<equiv>
+ (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
+ \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"
+
+Lemma is_biinv_type [type]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> 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 \<equiv> Equivalence.is_biinv {} {} f"
+
+translations "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f"
+
+Lemma is_biinvI:
+ assumes
+ "A: U i" "B: U i" "f: A \<rightarrow> B"
+ "g: B \<rightarrow> A" "h: B \<rightarrow> A"
+ "H1: g \<circ> f ~ id A" "H2: f \<circ> h ~ id B"
+ shows "is_biinv f"
+ unfolding is_biinv_def
+ proof intro
+ show "<g, H1>: \<Sum>g: B \<rightarrow> A. g \<circ> f ~ id A" by typechk
+ show "<h, H2>: \<Sum>g: B \<rightarrow> A. f \<circ> g ~ id B" by typechk
+ qed
+
+Lemma is_biinv_components [type]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_biinv f"
+ shows
+ section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
+ retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
+ ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
+ sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> 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 \<rightarrow> B"
+ shows "is_qinv f \<rightarrow> 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 \<rightarrow> B"
+ shows "is_biinv f \<rightarrow> is_qinv f"
+ apply intro
+ unfolding is_biinv_def apply elims
+ focus vars _ _ _ g H1 h H2
+ apply (rule is_qinvI)
+ \<^item> by (fact \<open>g: _\<close>)
+ \<^item> by (fact \<open>H1: _\<close>)
+ \<^item> proof -
+ have "g ~ g \<circ> (id B)" by compute refl
+ 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)
+ also note \<open>H2:_\<close>
+ finally show "f \<circ> g ~ id B" by this
+ qed
+ done
+ done
+
+Lemma (def) id_is_biinv:
+ "A: U i \<Longrightarrow> 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 \<rightarrow> B" "g: B \<rightarrow> C"
+ shows "is_biinv f \<rightarrow> is_biinv g \<rightarrow> is_biinv (g \<circ> 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 \<open>Equivalence\<close>
+
+text \<open>
+ Following the HoTT book, we first define equivalence in terms of
+ bi-invertibility.
+\<close>
+
+definition equivalence (infix "\<simeq>" 110)
+ where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f"
+
+Lemma equivalence_type [type]:
+ assumes "A: U i" "B: U i"
+ shows "A \<simeq> B: U i"
+ unfolding equivalence_def by typechk
+
+Lemma (def) equivalence_refl:
+ assumes "A: U i"
+ shows "A \<simeq> 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 \<simeq> B \<rightarrow> B \<simeq> 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 \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C"
+ proof intros
+ fix AB BC assume *: "AB: A \<simeq> B" "BC: B \<simeq> C"
+ then have
+ "fst AB: A \<rightarrow> B" and 1: "snd AB: is_biinv (fst AB)"
+ "fst BC: B \<rightarrow> C" and 2: "snd BC: is_biinv (fst BC)"
+ unfolding equivalence_def by typechk+
+ then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk
+ moreover have "is_biinv (fst BC \<circ> fst AB)"
+ using * unfolding equivalence_def by (rule funcomp_is_biinv 1 2) facts
+ ultimately show "A \<simeq> C"
+ unfolding equivalence_def by intro facts
+ qed
+
+text \<open>
+ 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.
+\<close>
+
+Lemma
+ assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+ shows "A \<simeq> B"
+ by (eq p) (rule equivalence_refl)
+
+text \<open>
+ The following proof is wordy because (1) typechecker normalization is still
+ rudimentary, and (2) we don't yet have universe level inference.
+\<close>
+
+Lemma (def) equiv_if_equal:
+ assumes
+ "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+ shows "<transp (id (U i)) p, ?isequiv>: A \<simeq> B"
+ unfolding equivalence_def
+ apply intro defer
+ \<^item> apply (eq p)
+ \<^enum> vars A B
+ apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
+ using [[solve_side_conds=1]]
+ apply (comp at B in "_ \<rightarrow> 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)
+ \<circ> by (rule Ui_in_USi)
+ \<circ> by compute (rule U_lift)
+ \<circ> by compute (rule id_is_biinv)
+ done
+ done
+
+ \<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close>
+ apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
+ using [[solve_side_conds=1]]
+ apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (rule transport, rule Ui_in_USi)
+ by (rule lift_universe_codomain, rule Ui_in_USi)
+ done
+
+
+end