From 3f7a8274271b4920e7eccd6f3b4cd516f6c55bd8 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 3 Mar 2019 22:53:45 +0100 Subject: Move definition of transport to Type_Families.thy, and change it to use meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly. --- Type_Families.thy | 115 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ Univalence.thy | 111 +++++++++++++++------------------------------------- 2 files changed, 147 insertions(+), 79 deletions(-) create mode 100644 Type_Families.thy diff --git a/Type_Families.thy b/Type_Families.thy new file mode 100644 index 0000000..b1e7686 --- /dev/null +++ b/Type_Families.thy @@ -0,0 +1,115 @@ +(******** +Isabelle/HoTT: Type families as fibrations +Feb 2019 + +Various results viewing type families as fibrations: transport, dependent map, path lifting etc. + +********) + +theory Type_Families +imports HoTT_Methods Sum Eq + +begin + + +section \Transport\ + +schematic_goal transport: + assumes [intro]: + "A: U i" "P: A \ U j" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: P x \ P y" +proof (path_ind' x y p) + show "\x. x: A \ id P x: P x \ P x" by derive +qed routine + +definition transport :: "[t \ t, t, t, t] \ t" ("(2transport[_, _, _] _)" [0, 0, 0, 1000]) +where "transport[P, x, y] p \ indEq (\a b. & (P a \ P b)) (\x. id P x) x y p" + +syntax "_transport'" :: "[t, t] \ t" ("(2_*)" [1000]) + +ML \val pretty_transport = Attrib.setup_config_bool @{binding "pretty_transport"} (K true)\ + +print_translation \ +let fun transport_tr' ctxt [P, x, y, p] = + if Config.get ctxt pretty_transport + then Syntax.const @{syntax_const "_transport'"} $ p + else @{const transport} $ P $ x $ y $ p +in + [(@{const_syntax transport}, transport_tr')] +end +\ + +corollary transport_type: + assumes "A: U i" "P: A \ U j" "x: A" "y: A" "p: x =[A] y" + shows "transport[P, x, y] p: P x \ P y" +unfolding transport_def using assms by (rule transport) + +lemma transport_comp: + assumes [intro]: "A: U i" "P: A \ U j" "a: A" + shows "transport P a a (refl a) \ id P a" +unfolding transport_def by derive + +declare + transport_type [intro] + transport_comp [comp] + +schematic_goal transport_invl: + assumes [intro]: + "P: A \ U j" "A: U i" + "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) =[P x \ P x] id P x" +proof (path_ind' x y p) + fix x assume [intro]: "x: A" + show + "refl (id P x) : + transport[P, x, x] (inv[A, x, x] (refl x)) o[P x] (transport[P, x, x] (refl x)) =[P x \ P x] + id P x" + by derive + + fix y p assume [intro]: "y: A" "p: x =[A] y" + show + "transport[P, y, x] (inv[A, x, y] p) o[P x] transport[P, x, y] p =[P x \ P x] id P x: U j" + by derive +qed + +schematic_goal transport_invr: + assumes [intro]: + "P: A \ U j" "A: U i" + "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)) =[P y \ P y] id P y" +proof (path_ind' x y p) + fix x assume [intro]: "x: A" + show + "refl (id P x) : + (transport[P, x, x] (refl x)) o[P x] transport[P, x, x] (inv[A, x, x] (refl x)) =[P x \ P x] + id P x" + by derive + + fix y p assume [intro]: "y: A" "p: x =[A] y" + show + "transport[P, x, y] p o[P y] transport[P, y, x] (inv[A, x, y] p) =[P y \ P y] id P y: U j" + by derive +qed + +(* The two proofs above are rather brittle: the assumption "P: A \ U j" needs to be put first + in order for the method derive to automatically work. +*) + +declare + transport_invl [intro] + transport_invr [intro] + + +schematic_goal path_lifting: + assumes + "A: U i" "P: A \ U j" + "u: P x" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: =[\x: A. P x] " +oops + + +end diff --git a/Univalence.thy b/Univalence.thy index 45818bb..30110f1 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -5,7 +5,7 @@ Feb 2019 ********) theory Univalence -imports HoTT_Methods Prod Sum Eq +imports HoTT_Methods Prod Sum Eq Type_Families begin @@ -114,24 +114,24 @@ section \Transport, homotopy, and bi-invertibility\ schematic_goal transport_invl_hom: assumes [intro]: - "A: U i" "P: A \ U j" + "P: A \ U j" "A: U i" "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" + (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 + 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" + "P: A \ U j" "A: U i" "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" + (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 + 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 @@ -139,21 +139,14 @@ declare transport_invr_hom [intro] text \ -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 somewhat of a challenge for current method automation. +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"}. +It is used in the derivation of @{text idtoeqv} in the next section. \ -lemma id_expand: assumes "A: U i" shows "A \ (id U i)`A" using assms by derive - -thm transport_invl_hom[where ?P="id U i"] - 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.\ + shows "?prf: biinv[A, B] (transport[Id, A, B] p)" +unfolding biinv_def apply (rule Sum_routine) prefer 2 apply (rule Sum_routine) @@ -161,40 +154,8 @@ prefer 2 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 derive - show "U i: U (Suc i)" by fact - - have "\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" - proof show "(id U i)`A: U i" by derive qed derive - have "\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" - apply rule prefer 3 apply (fact, derive) done - then 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" - by routine - - show "\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 "\g. g : (id U i)`B \ (id U i)`A \ - Eq.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 fact - qed derive - - fix g assume [intro]: "g: (id U i)`B \ (id U i)`A" - 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 - 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 derive +\ \The remaining subgoals are now handled easily\ +by derive section \Univalence\ @@ -205,15 +166,7 @@ schematic_goal type_eq_imp_equiv: unfolding equivalence_def apply (rule Prod_routine, rule Sum_routine) 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 derive +done (* Copy-paste the derived proof term as the definition of idtoeqv for now; should really have some automatic export of proof terms, though. @@ -221,26 +174,26 @@ qed derive definition idtoeqv :: "[ord, t, t] \ t" ("(2idtoeqv[_, _, _])") where " idtoeqv[i, A, B] \ \(p: A =[U i] B). - < transport (id U i) A B p, < - < transport (id U i) B A (inv[U i, A, B] p), - happly[x: (id U i)`A. (id U i)`A] - ((transport[id U i, B, A] (inv[U i, A, B] p)) o[(id U i)`A] transport[id U i, A, B] p) - (id (id U i)`A) + < transport (Id) A B p, < + < transport[Id, B, A] (inv[U i, A, B] p), + happly[x: A. A] + ((transport[Id, B, A] (inv[U i, A, B] p)) o[A] transport[Id, A, B] p) + (id A) (indEq (\A B p. - (transport[id U i, B, A] (inv[U i, A, B] p)) o[(id U i)`A] transport[id U i, A, B] p - =[(id U i)`A \ (id U i)`A] id (id U i)`A) - (\x. refl (id (id U i)`x)) A B p) + (transport[Id, B, A] (inv[U i, A, B] p)) o[A] transport[Id, A, B] p + =[A \ A] id A) + (\x. refl (id x)) A B p) >, - < transport (id U i) B A (inv[U i, A, B] p), - happly[x: (id U i)`B. (id U i)`B] - ((transport[id U i, A, B] p) o[(id U i)`B] (transport[id U i, B, A] (inv[U i, A, B] p))) - (id (id U i)`B) + < transport (Id) B A (inv[U i, A, B] p), + happly[x: B. B] + ((transport[Id, A, B] p) o[B] (transport[Id, B, A] (inv[U i, A, B] p))) + (id B) (indEq (\A B p. - transport[id U i, A, B] p o[(id U i)`B] (transport[id U i, B, A] (inv[U i, A, B] p)) - =[(id U i)`B \ (id U i)`B] id (id U i)`B) - (\x. refl (id (id U i)`x)) A B p) + transport[Id, A, B] p o[B] (transport[Id, B, A] (inv[U i, A, B] p)) + =[B \ B] id B) + (\x. refl (id x)) A B p) > > > @@ -249,7 +202,7 @@ idtoeqv[i, A, B] \ corollary idtoeqv_type: assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B" shows "idtoeqv[i, A, B]: A =[U i] B \ A \ B" -unfolding idtoeqv_def by (derive lems: type_eq_imp_equiv) +unfolding idtoeqv_def by (routine add: type_eq_imp_equiv) declare idtoeqv_type [intro] -- cgit v1.2.3