From 39b22fe12f0166d9516638204b4deabe22671d98 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 1 Mar 2019 00:44:58 +0100 Subject: Syntax changes. Transport inverse lemmas. --- Eq.thy | 88 ++++++++++++++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 70 insertions(+), 18 deletions(-) (limited to 'Eq.thy') diff --git a/Eq.thy b/Eq.thy index a89e56b..c6394dc 100644 --- a/Eq.thy +++ b/Eq.thy @@ -72,9 +72,9 @@ section \Properties of equality\ subsection \Symmetry (path inverse)\ definition inv :: "[t, t, t, t] \ t" -where "inv A x y p \ indEq (\x y. ^(y =[A] x)) (\x. refl x) x y p" +where "inv A x y p \ indEq (\x y. &(y =[A] x)) (\x. refl x) x y p" -syntax "_inv" :: "[t, t, t, t] \ t" ("(2inv[_, _, _] _)" [0, 0, 0, 1000]) +syntax "_inv" :: "[t, t, t, t] \ t" ("(2inv[_, _, _] _)" [0, 0, 0, 1000] 999) translations "inv[A, x, y] p" \ "(CONST inv) A x y p" syntax "_inv'" :: "t \ t" ("~_" [1000]) @@ -117,11 +117,12 @@ by definition pathcomp :: "[t, t, t, t, t, t] \ t" where "pathcomp A x y z p q \ (indEq - (\x y _. \z: A. y =[A] z \ x =[A] z) - (\x. \z: A. \q: x =[A] z. indEq (\x z _. x =[A] z) (\x. refl x) x z q) + (\x y. & \z: A. y =[A] z \ x =[A] z) + (\x. \z: A. \q: x =[A] z. indEq (\x z. & x =[A] z) (\x. refl x) x z q) x y p)`z`q" -syntax "_pathcomp" :: "[t, t, t, t, t, t] \ t" ("(2pathcomp[_, _, _, _] _ _)" [0, 0, 0, 0, 1000, 1000]) +syntax "_pathcomp" :: "[t, t, t, t, t, t] \ t" + ("(2pathcomp[_, _, _, _] _ _)" [0, 0, 0, 0, 1000, 1000] 999) translations "pathcomp[A, x, y, z] p q" \ "(CONST pathcomp) A x y z p q" syntax "_pathcomp'" :: "[t, t] \ t" (infixl "^" 110) @@ -139,12 +140,12 @@ in end \ -lemma pathcomp_type: +corollary pathcomp_type: assumes [intro]: "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" shows "pathcomp[A, x, y, z] p q: x =[A] z" unfolding pathcomp_def by (derive lems: transitivity) -lemma pathcomp_comp: +corollary pathcomp_comp: assumes [intro]: "A: U i" "a: A" shows "pathcomp[A, a, a, a] (refl a) (refl a) \ refl a" unfolding pathcomp_def by (derive lems: transitivity) @@ -276,7 +277,7 @@ in end \ -lemma ap_type: +corollary ap_type: assumes "A: U i" "B: U i" "f: A \ B" "x: A" "y: A" "p: x =[A] y" @@ -379,15 +380,15 @@ section \Transport\ schematic_goal transport: assumes [intro]: - "A: U i" "P: A \ U i" + "A: U i" "P: A \ U j" "x: A" "y: A" "p: x =[A] y" - shows "?prf: P x \ P 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 + 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" ("(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]) @@ -403,19 +404,70 @@ in end \ -lemma transport_type: - assumes "A: U i" "P: A \ U i" "x: A" "y: A" "p: x =[A] y" - shows "transport[P, x, y] p: P x \ P y" +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 i" "a: A" - shows "transport P a a (refl a) \ id (P a)" + 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]: + "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)" +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" + have [intro]: + "transport[P, y, x] (inv[A, x, y] p) o[P`x] transport[P, x, y] p : P`x \ P`x" + proof show "transport[P, x, y] p: P`x \ P`y" 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] id (P`x): U j" + by derive +qed + +schematic_goal transport_invr: + 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)) =[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" + have [intro]: + "transport[P, x, y] p o[P`y] transport[P, y, x] (inv[A, x, y] p): P`y \ P`y" + proof show "transport[P, x, y] p: P`x \ P`y" 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] id (P`y): U j" + by derive +qed + +declare + transport_invl [intro] + transport_invr [intro] end -- cgit v1.2.3