From c33f290df52e646edcf0589d98bd89da8ce288ec Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 1 Mar 2019 20:17:53 +0100 Subject: Proving transport is bi-invertible is harder than expected --- Univalence.thy | 170 +++++++++++++++++++++++++++++---------------------------- 1 file changed, 87 insertions(+), 83 deletions(-) (limited to 'Univalence.thy') diff --git a/Univalence.thy b/Univalence.thy index 04e1d67..42e452e 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -69,35 +69,6 @@ corollary happly_type: 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.\ @@ -139,73 +110,106 @@ unfolding equivalence_def proof (rule Sum_routine) qed (routine add: id_is_biinv) -section \Univalence\ +section \Transport, homotopy, and bi-invertibility\ -declare[[goals_limit=100, pretty_transport=true]] +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 -lemma lem: "\A. A: U i \ (id (U i))`A \ A" by derive +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 -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)" +declare + transport_invl_hom [intro] + transport_invr_hom [intro] + +(* +Next we derive a proof that the transport of an equality @{term p} is bi-invertible, with inverse given by the transport of the inverse @{text "~p"}. + +The proof is a challenge for current method automation, for two main reasons: +1. +*) -oops +declare[[pretty_transport=false, goals_limit=100]] -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 +lemma id_expand: "\A. A: U i \ A \ (id U i)`A" by derive +lemma id_contract: "\A. A: U i \ (id U i)`A \ A" by derive + +schematic_goal transport_biinv: + assumes [intro]: "p: A =[U i] B" "A: U i" "B: U i" + shows "?prf: biinv[A, B] (transport[id U i, A, B] p)" +apply (subst (0 2) id_expand, unfold biinv_def, fact+) + \ \Need to rewrite the first instances of @{term A} and @{term B} in order to + use the proofs of @{thm transport_invl_hom} and @{thm transport_invr_hom} later.\ 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) +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 can now be handled relatively easily.\ 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 - + show *: "U i: U (Suc i)" by derive + show "U i: U (Suc i)" by fact + + fix g assume [intro]: "g: (id U i)`B \ (id U i)`A" + + have + "transport (id U i) A B p o[(id U i)`B] g: (id U i)`B \ (id U i)`B" + proof show "(id U i)`A: U i" by derive qed derive + moreover have + "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" + apply rule prefer 3 apply (fact, derive) done + then show + "(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" + by routine + + have + "g o[(id U i)`A] transport (id U i) A B p: (id U i)`A \ (id U i)`A" + proof show "(id U i)`B: U i" by derive qed derive + moreover have + "g o[(id U i)`A] transport (id U i) A B p ~[x: (id U i)`A. (id U i)`A] id (id U i)`A: U i" + apply rule prefer 3 apply (fact, derive) done + then show + "g o[(id U i)`A] transport (id U i) A B p ~[x: (id U i)`A. (id U i)`A] id (id U i)`A: U i" + by routine + +qed + + +section \Univalence\ schematic_goal type_eq_imp_equiv: assumes [intro]: "A: U i" "B: U i" shows "?prf: (A =[U i] B) \ A \ B" unfolding equivalence_def apply (rule Prod_routine, rule Sum_routine) -prefer 2 - show *: "\f. f: A \ B \ isequiv[A, B] f: U i" - unfolding isequiv_def by (derive lems: assms - - show "\p. p: A =[U i] B \ transport p: A \ B" - by (derive lems: assms transport_type[where ?i="Suc i"] \ \Instantiate @{thm transport_type} with a suitable universe level here...\ - - show "\p. p: A =[U i] B \ ind\<^sub>= (\_. <\x. refl x>, \x. refl x>>) p: isequiv[A, B] (transport p)" - proof (elim Equal_elim) - show "\T. T: U i \ <\x. refl x>, \x. refl x>>: isequiv[T, T] (transport (refl T))" - by (derive lems: transport_comp[where ?i="Suc i" and ?A="U i"] id_isequiv) - \ \...and also here.\ - - show "\A B p. \A: U i; B: U i; p: A =[U i] B\ \ isequiv[A, B] (transport p): U i" - unfolding isequiv_def by (derive lems: assms transport_type - qed fact+ -qed (derive lems: assms +prefer 3 apply (derive lems: transport_biinv) +proof - + fix p assume [intro]: "p: A =[U i] B" + have + "transport (id U i) A B p: (id U i)`A \ (id U i)`B" + proof show "U i: U(Suc i)" by hierarchy qed derive + moreover have [intro]: + "(id U i)`A \ (id U i)`B \ A \ B" by derive + ultimately show "transport (id U i) A B p: A \ B" by simp +qed deriv (* section \The univalence axiom\ -- cgit v1.2.3