From 6dd1b27f7f84b17ad88e5b382042bd0c577a92f4 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 8 Mar 2019 19:33:24 +0100 Subject: prune import lists --- Projections.thy | 2 +- Type_Families.thy | 2 +- Univalence.thy | 159 +++--------------------------------------------------- 3 files changed, 10 insertions(+), 153 deletions(-) diff --git a/Projections.thy b/Projections.thy index 9eeb57f..a28c66b 100644 --- a/Projections.thy +++ b/Projections.thy @@ -7,7 +7,7 @@ Projection functions for the dependent sum type. ********) theory Projections -imports HoTT_Methods Prod Sum +imports Prod Sum begin diff --git a/Type_Families.thy b/Type_Families.thy index 6c784e5..b9e1049 100644 --- a/Type_Families.thy +++ b/Type_Families.thy @@ -7,7 +7,7 @@ Various results viewing type families as fibrations: transport, path lifting, de ********) theory Type_Families -imports HoTT_Methods Sum Projections Eq +imports Eq Projections begin diff --git a/Univalence.thy b/Univalence.thy index 322dbbd..dd8a13c 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -5,158 +5,14 @@ Feb 2019 ********) theory Univalence -imports HoTT_Methods Prod Sum Eq Type_Families +imports Equivalence begin -section \Homotopy\ - -definition homotopic :: "[t, t \ t, t, t] \ t" ("(2homotopic[_, _] _ _)" [0, 0, 1000, 1000]) -where "homotopic[A, B] f g \ \x: A. f`x =[B x] g`x" - -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)\ - -print_translation \ -let fun homotopic_tr' ctxt [A, B, f, g] = - if Config.get ctxt pretty_homotopic - then Syntax.const @{syntax_const "_homotopic'"} $ f $ g - else @{const homotopic} $ A $ B $ f $ g -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" - shows "f ~[x: A. B x] g: U i" -by derive - -declare homotopic_type [intro] - -schematic_goal fun_eq_imp_homotopic: - 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_homotopic) - - -section \Equivalence\ - -text \For now, we define equivalence in terms of 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 homotopic 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 \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"}. -It is used in the derivation of @{text idtoeqv} in the next section. -\ - -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 - - -section \Univalence\ - schematic_goal type_eq_imp_equiv: assumes [intro]: "A: U i" "B: U i" - shows "?prf: A =[U i] B \ A \ B" + shows "?prf: A =[U i] B \ A \ B" unfolding equivalence_def apply (rule Prod_routine, rule Sum_routine) prefer 3 apply (derive lems: transport_biinv) @@ -195,15 +51,16 @@ 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" + shows "idtoeqv[i, A, B]: A =[U i] B \ A \ B" unfolding idtoeqv_def by (routine add: type_eq_imp_equiv) declare idtoeqv_type [intro] -(* I'll formalize a more explicit constructor for the inverse equivalence of idtoeqv later; - the following is a placeholder for now. -*) -axiomatization ua :: "[ord, t, t] \ t" where univalence: "ua i A B: biinv[A, B] idtoeqv[i, A, B]" + +text \For now, we use bi-invertibility as our definition of equivalence.\ + +axiomatization univalance :: "[ord, t, t] \ t" +where univalence: "univalence i A B: biinv[A, B] idtoeqv[i, A, B]" end -- cgit v1.2.3