From 85fc133fa0d64c61c380fcecada8f8358ad4b773 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 1 Mar 2019 15:45:10 +0100 Subject: transport and homotopy --- Univalence.thy | 101 +++++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 80 insertions(+), 21 deletions(-) (limited to 'Univalence.thy') diff --git a/Univalence.thy b/Univalence.thy index e073e50..04e1d67 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -20,6 +20,7 @@ declare homotopic_def [comp] syntax "_homotopic" :: "[t, idt, t, t, t] \ t" ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100) translations "f ~[x: A. B] g" \ "(CONST homotopic) A (\x. B) f g" +(* syntax "_homotopic'" :: "[t, t] \ t" ("(2_ ~ _)" [1000, 1000]) ML \val pretty_homotopic = Attrib.setup_config_bool @{binding "pretty_homotopic"} (K true)\ @@ -33,6 +34,7 @@ in [(@{const_syntax homotopic}, homotopic_tr')] end \ +*) lemma homotopic_type: assumes [intro]: "A: U i" "B: A \ U i" "f: \x: A. B x" "g: \x: A. B x" @@ -43,26 +45,59 @@ declare homotopic_type [intro] schematic_goal fun_eq_imp_homotopic: assumes [intro]: - "A: U i" "B: A \ U i" - "f: \x: A. B x" "g: \x: A. B x" "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" ("(2happly[_, _] _ _ _)" [0, 0, 1000, 1000, 1000]) -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" +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]: - "A: U i" "B: A \ U i" - "f: \x: A. B x" "g: \x: A. B x" "p: f =[\x: A. B x] g" - shows "happly[A, B] f g 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_homotopic) +section \Transport and homotopy\ + +schematic_goal transport_invl_hom: + assumes [intro]: + "A: U i" "P: A \ U j" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: + (transport[P, y, x] (inv[A, x, y] p)) o[P`x] (transport[P, x, y] p) ~[w: P`x. P`x] id(P`x)" +proof (rule happly_type[OF transport_invl]) + show "(transport[P, y, x] (inv[A, x, y] p)) o[P`x] (transport[P, x, y] p): P`x \ P`x" + proof show "P`y: U j" by routine qed routine +qed routine + +schematic_goal transport_invr_hom: + assumes [intro]: + "A: U i" "P: A \ U j" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: + (transport[P, x, y] p) o[P`y] (transport[P, y, x] (inv[A, x, y] p)) ~[w: P`y. P`y] id(P`y)" +proof (rule happly_type[OF transport_invr]) + show "(transport[P, x, y] p) o[P`y] (transport[P, y, x] (inv[A, x, y] p)): P`y \ P`y" + proof show "P`x: U j" by routine qed routine +qed routine + +declare + transport_invl_hom [intro] + transport_invr_hom [intro] + + section \Equivalence\ text \For now, we define equivalence in terms of bi-invertibility.\ @@ -106,23 +141,47 @@ qed (routine add: id_is_biinv) section \Univalence\ -(* +declare[[goals_limit=100, pretty_transport=true]] + +lemma lem: "\A. A: U i \ (id (U i))`A \ A" by derive + schematic_goal assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B" shows "?prf: biinv[A, B] (transport[id(U i), A, B] p)" +apply (path_ind' A B p) +apply (unfold biinv_def) + show "?a : biinv[A, B] (transport[id(U i), A, B] p)" + +oops + +schematic_goal + assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B" + shows "?prf: biinv[id(U i)`A, id(U i)`B] (transport[id(U i), A, B] p)" unfolding biinv_def -apply (rule Sum_routine) defer -apply (rule Sum_intro) - have - "transport[id(U i), A, B] p: (id (U i))`A \ (id (U i))`B" - by (derive lems: transport_type[where ?A="U i"] - moreover have - "(id (U i))`A \ (id (U i))`B \ A \ B" by deriv - ultimately have [intro]: - "transport[id(U i), A, B] p: A \ B" by simp - - show "\g: B \ A. (transport[id(U i), A, B] p o[B] g) ~[x: B. B] (id B) : U i" - by deriv +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) +proof - + show "U i: U (Suc i)" by hierarchy + show "U i: U (Suc i)" by hierarchy + show "\g. g : id (U i)`B \ id (U i)`A \ (transport[id(U i), A, B] p) o[id (U i)`B] g ~[x: id (U i)`B. id (U i)`B] id (id (U i)`B) : U i" + proof + show "id (U i)`B : U i" by derive + show "id (U i)`B : U i" by derive + show "id (id (U i)`B) : id (U i)`B \ id (U i)`B" by derive + show + "\g. g : id (U i)`B \ id (U i)`A \ + (transport[id(U i), A, B] p) o[id (U i)`B] g: id (U i)`B \ id (U i)`B" + apply rule + prefer 4 apply assumption + proof - + show "id (U i)`B : U i" by derive + show "id (U i)`A : U i" by derive + show "id (U i)`B : U i" by derive + +oops schematic_goal type_eq_imp_equiv: @@ -148,7 +207,7 @@ prefer 2 qed fact+ qed (derive lems: assms - +(* section \The univalence axiom\ axiomatization univalence :: "[t, t] \ t" where UA: "univalence A B: isequiv[A, B] idtoeqv" -- cgit v1.2.3