From 45c3879db6850282bc067318e31cccf42e60ac8f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 26 Mar 2019 17:04:01 +0100 Subject: working towards biinv_imp_qinv --- Equivalence.thy | 197 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 197 insertions(+) create mode 100644 Equivalence.thy (limited to 'Equivalence.thy') diff --git a/Equivalence.thy b/Equivalence.thy new file mode 100644 index 0000000..b8df15d --- /dev/null +++ b/Equivalence.thy @@ -0,0 +1,197 @@ +(******** +Isabelle/HoTT: Quasi-inverse and equivalence +Mar 2019 + +********) + +theory Equivalence +imports Type_Families + +begin + +section \Homotopy\ + +definition homotopy :: "[t, t \ t, t, t] \ t" ("(2homotopy[_, _] _ _)" [0, 0, 1000, 1000]) +where "homotopy[A, B] f g \ \x: A. f`x =[B x] g`x" + +declare homotopy_def [comp] + +syntax "_homotopy" :: "[t, idt, t, t, t] \ t" ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100) +translations "f ~[x: A. B] g" \ "(CONST homotopy) A (\x. B) f g" + +lemma homotopy_type: + assumes [intro]: "A: U i" "B: A \ U i" "f: \x: A. B x" "g: \x: A. B x" + shows "f ~[x: A. B x] g: U i" +by derive + +declare homotopy_type [intro] + +text \Homotopy inverse and composition (symmetry and transitivity):\ + +definition hominv :: "[t, t \ t, t, t] \ t" ("(2hominv[_, _, _, _])") +where "hominv[A, B, f, g] \ \H: f ~[x: A. B x] g. \x: A. inv[B x, f`x, g`x]`(H`x)" + +lemma hominv_type: + assumes [intro]: "A: U i" "B: A \ U i" "f: \x: A. B x" "g: \x: A. B x" + shows "hominv[A, B, f, g]: f ~[x: A. B x] g \ g ~[x: A. B x] f" +unfolding hominv_def by (derive, fold homotopy_def)+ derive + +definition homcomp :: "[t, t \ t, t, t, t] \ t" ("(2homcomp[_, _, _, _, _])") where + "homcomp[A, B, f, g, h] \ \H: f ~[x: A. B x] g. \H': g ~[x: A. B x] h. + \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 \ U i" + "f: \x: A. B x" "g: \x: A. B x" "h: \x: A. B x" + shows "homcomp[A, B, f, g, h]: f ~[x: A. B x] g \ g ~[x: A. B x] h \ 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 =[\x: A. B x] g" + "f: \x: A. B x" "g: \x: A. B x" + "A: U i" "B: A \ U i" + shows "?prf: f ~[x: A. B x] g" +proof (path_ind' f g p) + show "\f. f : \(x: A). B x \ \x: A. refl(f`x): f ~[x: A. B x] f" by derive +qed routine + +definition happly :: "[t, t \ t, t, t, t] \ t" +where "happly A B f g p \ indEq (\f g. & f ~[x: A. B x] g) (\f. \(x: A). refl(f`x)) f g p" + +syntax "_happly" :: "[idt, t, t, t, t, t] \ t" + ("(2happly[_: _. _] _ _ _)" [0, 0, 0, 1000, 1000, 1000]) +translations "happly[x: A. B] f g p" \ "(CONST happly) A (\x. B) f g p" + +corollary happly_type: + assumes [intro]: + "p: f =[\x: A. B x] g" + "f: \x: A. B x" "g: \x: A. B x" + "A: U i" "B: A \ 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 \Homotopy and function composition:\ + +declare[[pretty_compose=false]] + +schematic_goal composition_homotopyl: + assumes [intro]: + "H: f ~[x: A. B] g" + "f: A \ B" "g: A \ B" "h: B \ 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 (derive, fold homotopy_def, fact+) +qed routine + +section \Bi-invertibility\ + +definition biinv :: "[t, t, t] \ t" ("(2biinv[_, _]/ _)") +where "biinv[A, B] f \ + (\g: B \ A. g o[A] f ~[x:A. A] id A) \ (\g: B \ A. f o[B] g ~[x: B. B] id B)" + +text \ +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 "\x:A. B x"}. +\<^item> @{term "biinv[A, B] f"} expresses that the function @{term f} of type @{term "A \ B"} is bi-invertible. +\ + +lemma biinv_type: + assumes [intro]: "A: U i" "B: U i" "f: A \ 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, compute) + show "x: A. refl x>: \(g: A \ A). (g o[A] id A) ~[x: A. A] (id A)" by derive + show "x: A. refl x>: \(g: A \ A). (id A o[A] g) ~[x: A. A] (id A)" by derive +qed routine + +definition equivalence :: "[t, t] \ t" (infix "\" 100) +where "A \ B \ \f: A \ B. biinv[A, B] f" + +schematic_goal equivalence_symmetric: + assumes [intro]: "A: U i" + shows "?prf: A \ A" +unfolding equivalence_def proof (rule Sum_routine) + show "\f. f : A \ A \ biinv[A, A] f : U i" unfolding biinv_def by derive + show "id A: A \ A" by routine +qed (routine add: id_is_biinv) + + +section \Quasi-inverse\ + +definition qinv :: "[t, t, t] \ t" ("(2qinv[_, _]/ _)") +where "qinv[A, B] f \ \g: B \ A. (g o[A] f ~[x: A. A] id A) \ (f o[B] g ~[x: B. B] id B)" + +schematic_goal biinv_imp_qinv: + assumes [intro]: "A: U i" "B: U i" "f: A \ B" + shows "?prf: (biinv[A, B] f) \ (qinv[A,B] f)" +proof (rule Prod_routine) +assume "b: biinv[A, B] f" +define g H g' H' where + "g \ fst[B \ A, \g. g o[A] f ~[x: A. A] id A] ` + (fst[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" +and + "H \ snd[B \ A, \g. g o[A] f ~[x: A. A] id A] ` + (fst[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" +and + "g' \ fst[B \ A, \g. f o[B] g ~[x: B. B] id B] ` + (snd[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" +and + "H' \ snd[B \ A, \g. f o[B] g ~[x: B. B] id B] ` + (snd[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" + +have "g o[B] (f o[B] g') \ g" +unfolding g_def g'_def proof compute + + +section \Transport, homotopy, and bi-invertibility\ + +schematic_goal transport_invl_hom: + assumes [intro]: + "P: A \ 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 \ 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 \ +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"}. +\ + +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) +\ \The remaining subgoals are now handled easily\ +by derive + + +end -- cgit v1.2.3