diff options
Diffstat (limited to 'Equivalence.thy')
| -rw-r--r-- | Equivalence.thy | 228 |
1 files changed, 0 insertions, 228 deletions
diff --git a/Equivalence.thy b/Equivalence.thy deleted file mode 100644 index 07ef0df..0000000 --- a/Equivalence.thy +++ /dev/null @@ -1,228 +0,0 @@ -(******** -Isabelle/HoTT: Quasi-inverse and equivalence -Mar 2019 - -********) - -theory Equivalence -imports Type_Families - -begin - -section \<open>Homotopy\<close> - -definition homotopy :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t" ("(2homotopy[_, _] _ _)" [0, 0, 1000, 1000]) -where "homotopy[A, B] f g \<equiv> \<Prod>x: A. f`x =[B x] g`x" - -declare homotopy_def [comp] - -syntax "_homotopy" :: "[t, idt, t, t, t] \<Rightarrow> t" ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100) -translations "f ~[x: A. B] g" \<rightleftharpoons> "(CONST homotopy) A (\<lambda>x. B) f g" - -lemma homotopy_type: - assumes [intro]: "A: U i" "B: A \<leadsto> U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" - shows "f ~[x: A. B x] g: U i" -by derive - -declare homotopy_type [intro] - -text \<open>Homotopy inverse and composition (symmetry and transitivity):\<close> - -definition hominv :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t" ("(2hominv[_, _, _, _])") -where "hominv[A, B, f, g] \<equiv> \<lambda>H: f ~[x: A. B x] g. \<lambda>x: A. inv[B x, f`x, g`x]`(H`x)" - -lemma hominv_type: - assumes [intro]: "A: U i" "B: A \<leadsto> U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" - shows "hominv[A, B, f, g]: f ~[x: A. B x] g \<rightarrow> g ~[x: A. B x] f" -unfolding hominv_def by (derive, fold homotopy_def)+ derive - -definition homcomp :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" ("(2homcomp[_, _, _, _, _])") where - "homcomp[A, B, f, g, h] \<equiv> \<lambda>H: f ~[x: A. B x] g. \<lambda>H': g ~[x: A. B x] h. - \<lambda>x: A. pathcomp[B x, f`x, g`x, h`x]`(H`x)`(H'`x)" - -lemma homcomp_type: - assumes [intro]: - "A: U i" "B: A \<leadsto> U i" - "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" "h: \<Prod>x: A. B x" - shows "homcomp[A, B, f, g, h]: f ~[x: A. B x] g \<rightarrow> g ~[x: A. B x] h \<rightarrow> f ~[x: A. B x] h" -unfolding homcomp_def by (derive, fold homotopy_def)+ derive - -schematic_goal fun_eq_imp_homotopy: - assumes [intro]: - "p: f =[\<Prod>x: A. B x] g" - "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" - "A: U i" "B: A \<leadsto> U i" - shows "?prf: f ~[x: A. B x] g" -proof (path_ind' f g p) - show "\<And>f. f : \<Prod>(x: A). B x \<Longrightarrow> \<lambda>x: A. refl(f`x): f ~[x: A. B x] f" by derive -qed routine - -definition happly :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" -where "happly A B f g p \<equiv> indEq (\<lambda>f g. & f ~[x: A. B x] g) (\<lambda>f. \<lambda>(x: A). refl(f`x)) f g p" - -syntax "_happly" :: "[idt, t, t, t, t, t] \<Rightarrow> t" - ("(2happly[_: _. _] _ _ _)" [0, 0, 0, 1000, 1000, 1000]) -translations "happly[x: A. B] f g p" \<rightleftharpoons> "(CONST happly) A (\<lambda>x. B) f g p" - -corollary happly_type: - assumes [intro]: - "p: f =[\<Prod>x: A. B x] g" - "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" - "A: U i" "B: A \<leadsto> U i" - shows "happly[x: A. B x] f g p: f ~[x: A. B x] g" -unfolding happly_def by (derive lems: fun_eq_imp_homotopy) - -text \<open>Homotopy and function composition:\<close> - -schematic_goal composition_homl: - assumes [intro]: - "H: f ~[x: A. B] g" - "f: A \<rightarrow> B" "g: A \<rightarrow> B" "h: B \<rightarrow> C" - "A: U i" "B: U i" "C: U i" - shows "?prf: h o[A] f ~[x: A. C] h o[A] g" -unfolding homotopy_def compose_def proof (rule Prod_routine, subst (0 1) comp) - fix x assume [intro]: "x: A" - show "ap[h, B, C, f`x, g`x]`(H`x): h`(f`x) =[C] h`(g`x)" by (routine, fold homotopy_def, fact+) -qed routine - -schematic_goal composition_homr: - assumes [intro]: - "H: f ~[x: B. C] g" - "h: A \<rightarrow> B" "f: B \<rightarrow> C" "g: B \<rightarrow> C" - "A: U i" "B: U i" "C: U i" - shows "?prf: f o[A] h ~[x: A. C] g o[A] h" -unfolding homotopy_def compose_def proof (rule Prod_routine, subst (0 1) comp) - fix x assume [intro]: "x: A" - show "H`(h`x): f`(h`x) =[C] g`(h`x)" by (routine, fold homotopy_def, routine) -qed routine - - -section \<open>Bi-invertibility\<close> - -definition biinv :: "[t, t, t] \<Rightarrow> t" ("(2biinv[_, _]/ _)") -where "biinv[A, B] f \<equiv> - (\<Sum>g: B \<rightarrow> A. g o[A] f ~[x:A. A] id A) \<times> (\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: B. B] id B)" - -text \<open> -The meanings of the syntax defined above are: -\<^item> @{term "f ~[x: A. B x] g"} expresses that @{term f} and @{term g} are homotopy functions of type @{term "\<Prod>x:A. B x"}. -\<^item> @{term "biinv[A, B] f"} expresses that the function @{term f} of type @{term "A \<rightarrow> B"} is bi-invertible. -\<close> - -lemma biinv_type: - assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" - shows "biinv[A, B] f: U i" -unfolding biinv_def by derive - -declare biinv_type [intro] - -schematic_goal id_is_biinv: - assumes [intro]: "A: U i" - shows "?prf: biinv[A, A] (id A)" -unfolding biinv_def proof (rule Sum_routine) - show "<id A, \<lambda>x: A. refl x>: \<Sum>(g: A \<rightarrow> A). (g o[A] id A) ~[x: A. A] (id A)" by derive - show "<id A, \<lambda>x: A. refl x>: \<Sum>(g: A \<rightarrow> A). (id A o[A] g) ~[x: A. A] (id A)" by derive -qed derive - -definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<cong>" 100) -where "A \<cong> B \<equiv> \<Sum>f: A \<rightarrow> B. biinv[A, B] f" - -schematic_goal equivalence_symmetric: - assumes [intro]: "A: U i" - shows "?prf: A \<cong> A" -unfolding equivalence_def proof (rule Sum_routine) - show "\<And>f. f : A \<rightarrow> A \<Longrightarrow> biinv[A, A] f : U i" unfolding biinv_def by derive - show "id A: A \<rightarrow> A" by routine -qed (routine add: id_is_biinv) - - -section \<open>Quasi-inverse\<close> - -definition qinv :: "[t, t, t] \<Rightarrow> t" ("(2qinv[_, _]/ _)") -where "qinv[A, B] f \<equiv> \<Sum>g: B \<rightarrow> A. (g o[A] f ~[x: A. A] id A) \<times> (f o[B] g ~[x: B. B] id B)" - -schematic_goal biinv_imp_qinv: - assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" - shows "?prf: (biinv[A, B] f) \<rightarrow> (qinv[A,B] f)" -proof (rule Prod_routine) - -assume [intro]: "b: biinv[A, B] f" - -text \<open>Components of the witness of biinvertibility of @{term f}:\<close> - -let ?fst_of_b = - "fst[\<Sum>g: B \<rightarrow> A. g o[A] f ~[x: A. A] id A, &\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: B. B] id B]" -and ?snd_of_b = - "snd[\<Sum>g: B \<rightarrow> A. g o[A] f ~[x: A. A] id A, &\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: B. B] id B]" - -define g H g' H' where - "g \<equiv> fst[B \<rightarrow> A, \<lambda>g. g o[A] f ~[x: A. A] id A] ` (?fst_of_b ` b)" and - "H \<equiv> snd[B \<rightarrow> A, \<lambda>g. g o[A] f ~[x: A. A] id A] ` (?fst_of_b ` b)" and - "g' \<equiv> fst[B \<rightarrow> A, \<lambda>g. f o[B] g ~[x: B. B] id B] ` (?snd_of_b ` b)" and - "H' \<equiv> snd[B \<rightarrow> A, \<lambda>g. f o[B] g ~[x: B. B] id B] ` (?snd_of_b ` b)" - -have "H: g o[A] f ~[x: A. A] id A" -unfolding H_def g_def proof standard+ - have - "fst[\<Sum>(g: B \<rightarrow> A). g o[A] f ~[x: A. A] id A, &\<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B] : - (biinv[A, B] f) \<rightarrow> (\<Sum>(g: B \<rightarrow> A). g o[A] f ~[g: A. A] id A)" unfolding biinv_def by derive - thus - "fst[\<Sum>(g: B \<rightarrow> A). g o[A] f ~[x: A. A] id A, &\<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B]`b : - \<Sum>(g: B \<rightarrow> A). g o[A] f ~[g: A. A] id A" by derive rule -qed derive - -moreover have "(id A) o[B] g' \<equiv> g'" proof derive - show "g': B \<rightarrow> A" unfolding g'_def proof - have - "snd[\<Sum>(g: B \<rightarrow> A). g o[A] f ~[x: A. A] id A, &\<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B] : - (biinv[A, B] f) \<rightarrow> (\<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B)" unfolding biinv_def by derive - thus - "snd[\<Sum>(g: B \<rightarrow> A). g o[A] f ~[x: A. A] id A, &\<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B]`b : - \<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B" by derive rule - qed derive -qed - - - -section \<open>Transport, homotopy, and bi-invertibility\<close> - -schematic_goal transport_invl_hom: - assumes [intro]: - "P: A \<leadsto> U j" "A: U i" - "x: A" "y: A" "p: x =[A] y" - shows "?prf: - (transport[A, P, y, x]`(inv[A, x, y]`p)) o[P x] (transport[A, P, x, y]`p) ~[w: P x. P x] id P x" -by (rule happly_type[OF transport_invl], derive) - -schematic_goal transport_invr_hom: - assumes [intro]: - "A: U i" "P: A \<leadsto> U j" - "y: A" "x: A" "p: x =[A] y" - shows "?prf: - (transport[A, P, x, y]`p) o[P y] (transport[A, P, y, x]`(inv[A, x, y]`p)) ~[w: P y. P y] id P y" -by (rule happly_type[OF transport_invr], derive) - -declare - transport_invl_hom [intro] - transport_invr_hom [intro] - -text \<open> -The following result states that the transport of an equality @{term p} is bi-invertible, with inverse given by the transport of the inverse @{text "~p"}. -\<close> - -schematic_goal transport_biinv: - assumes [intro]: "p: A =[U i] B" "A: U i" "B: U i" - shows "?prf: biinv[A, B] (transport[U i, Id, A, B]`p)" -unfolding biinv_def -apply (rule Sum_routine) -prefer 2 - apply (rule Sum_routine) - prefer 3 apply (rule transport_invl_hom) -prefer 9 - apply (rule Sum_routine) - prefer 3 apply (rule transport_invr_hom) -\<comment> \<open>The remaining subgoals are now handled easily\<close> -by derive - - -end |