From 8f7164976d08446e77a0e1eceaaa01f0ed363e5b Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 6 Mar 2019 11:42:19 +0100 Subject: Make functions object-level --- Type_Families.thy | 80 ++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 53 insertions(+), 27 deletions(-) (limited to 'Type_Families.thy') diff --git a/Type_Families.thy b/Type_Families.thy index b1e7686..f874e3d 100644 --- a/Type_Families.thy +++ b/Type_Families.thy @@ -7,7 +7,7 @@ Various results viewing type families as fibrations: transport, dependent map, p ********) theory Type_Families -imports HoTT_Methods Sum Eq +imports HoTT_Methods Sum Projections Eq begin @@ -23,31 +23,31 @@ 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" +definition transport :: "[t, t \ t, t, t] \ t" ("(2transport[_, _, _, _])") +where "transport[A, P, x, y] \ \p: x =[A] y. indEq (\a b. & (P a \ P b)) (\x. id P x) x y p" -syntax "_transport'" :: "[t, t] \ t" ("(2_*)" [1000]) +syntax "_transport'" :: "t \ t" ("transport[_]") ML \val pretty_transport = Attrib.setup_config_bool @{binding "pretty_transport"} (K true)\ print_translation \ -let fun transport_tr' ctxt [P, x, y, p] = +let fun transport_tr' ctxt [A, P, x, y] = if Config.get ctxt pretty_transport - then Syntax.const @{syntax_const "_transport'"} $ p - else @{const transport} $ P $ x $ y $ p + then Syntax.const @{syntax_const "_transport'"} $ P + else @{const transport} $ A $ P $ x $ y 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) + assumes [intro]: "A: U i" "P: A \ U j" "x: A" "y: A" "p: x =[A] y" + shows "transport[A, P, x, y]`p: P x \ P y" +unfolding transport_def by derive lemma transport_comp: assumes [intro]: "A: U i" "P: A \ U j" "a: A" - shows "transport P a a (refl a) \ id P a" + shows "transport[A, P, a, a]`(refl a) \ id P a" unfolding transport_def by derive declare @@ -56,59 +56,85 @@ declare schematic_goal transport_invl: assumes [intro]: - "P: A \ U j" "A: U i" + "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) =[P x \ P x] id P x" + (transport[A, P, y, x]`(inv[A, x, y]`p)) o[P x] (transport[A, 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] + transport[A, P, x, x]`(inv[A, x, x]`(refl x)) o[P x] (transport[A, 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" + "transport[A, P, y, x]`(inv[A, x, y]`p) o[P x] transport[A, 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" + "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)) =[P y \ P y] id P y" + (transport[A, P, x, y]`p) o[P y] (transport[A, 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" + (transport[A, P, x, x]`(refl x)) o[P x] transport[A, 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" + "transport[A, P, x, y]`p o[P y] transport[A, 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" + assumes [intro]: + "P: A \ U i" "A: U i" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: \u: P x. =[\x: A. P x] " +proof (path_ind' x y p, rule Prod_routine) + fix x u assume [intro]: "x: A" "u: P x" + have "(transport[A, P, x, x]`(refl x))`u \ u" by derive + thus "(refl ): =[\(x: A). P x] " + proof simp qed routine +qed routine + +definition lift :: "[t, t \ t, t, t] \ t" ("(2lift[_, _, _, _])") +where + "lift[A, P, x, y] \ \u: P x. \p: x =[A] y. (indEq + (\x y p. \u: P x. =[\(x: A). P x] ) + (\x. \(u: P x). refl ) x y p)`u" + +corollary lift_type: + assumes [intro]: + "P: A \ U i" "A: U i" + "x: A" "y: A" "p: x =[A] y" "u: P x" + shows "lift[A, P, x, y]`u`p: =[\x: A. P x] " +unfolding lift_def by (derive lems: path_lifting) + +schematic_goal lift_comp: + assumes [intro]: + "P: A \ U i" "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: =[\x: A. P x] " + "u: P x" + defines "Fst \ ap[fst[A, P], \x: A. P x, A, , ]" + shows "?prf: Fst`(lift[A, P, x, y]`u`p) =[x =[A] y] p" +proof derive oops -- cgit v1.2.3