From 22c4bbccf47e53160db5ae5856de6fed9045b22c Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 8 Mar 2019 17:26:25 +0100 Subject: type lemmas for derived functions should type the functions themselves --- Eq.thy | 22 +++++++---- Type_Families.thy | 109 +++++++++++++++++++++++++++++++++++++++++++----------- 2 files changed, 102 insertions(+), 29 deletions(-) diff --git a/Eq.thy b/Eq.thy index ca03089..dd92fce 100644 --- a/Eq.thy +++ b/Eq.thy @@ -98,7 +98,7 @@ in end \ -lemma inv_type: "\A: U i; x: A; y: A; p: x =[A] y\ \ inv[A, x, y]`p: y =[A] x" +lemma inv_type: "\A: U i; x: A; y: A\ \ inv[A, x, y]: x =[A] y \ y =[A] x" unfolding inv_def by derive lemma inv_comp: "\A: U i; a: A\ \ inv[A, a, a]`(refl a) \ refl a" @@ -146,8 +146,8 @@ end \ 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" + assumes [intro]: "A: U i" "x: A" "y: A" "z: A" + shows "pathcomp[A, x, y, z]: x =[A] y \ y =[A] z \ x =[A] z" unfolding pathcomp_def by (derive lems: transitivity) corollary pathcomp_comp: @@ -278,21 +278,27 @@ in end \ -corollary ap_type: +corollary ap_typ: + assumes [intro]: + "A: U i" "B: U i" "f: A \ B" + "x: A" "y: A" + shows "ap[f, A, B, x, y]: x =[A] y \ f`x =[B] f`y" +unfolding ap_def by routine + +corollary ap_app_typ: assumes [intro]: "A: U i" "B: U i" "f: A \ B" "x: A" "y: A" "p: x =[A] y" shows "ap[f, A, B, x, y]`p: f`x =[B] f`y" -unfolding ap_def by routine +by (routine add: ap_typ) lemma ap_comp: assumes [intro]: "A: U i" "B: U i" "f: A \ B" "x: A" shows "ap[f, A, B, x, x]`(refl x) \ refl (f`x)" unfolding ap_def by derive -declare - ap_type [intro] - ap_comp [comp] +lemmas ap_type [intro] = ap_typ ap_app_typ +lemmas ap_comp [comp] schematic_goal ap_func_pathcomp: diff --git a/Type_Families.thy b/Type_Families.thy index f874e3d..6c784e5 100644 --- a/Type_Families.thy +++ b/Type_Families.thy @@ -2,7 +2,7 @@ Isabelle/HoTT: Type families as fibrations Feb 2019 -Various results viewing type families as fibrations: transport, dependent map, path lifting etc. +Various results viewing type families as fibrations: transport, path lifting, dependent map etc. ********) @@ -41,8 +41,8 @@ end \ corollary transport_type: - 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" + assumes [intro]: "A: U i" "P: A \ U j" "x: A" "y: A" + shows "transport[A, P, x, y]: x =[A] y \ P x \ P y" unfolding transport_def by derive lemma transport_comp: @@ -64,14 +64,14 @@ proof (path_ind' x y p) fix x assume [intro]: "x: A" show "refl (id 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" + 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[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" + "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 @@ -91,8 +91,8 @@ proof (path_ind' x y p) fix y p assume [intro]: "y: A" "p: x =[A] y" show - "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" + "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 @@ -101,41 +101,108 @@ declare transport_invr [intro] +section \Path lifting\ + schematic_goal path_lifting: 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] " + 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] " + 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 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] " + "x: A" "y: A" + shows + "lift[A, P, x, y]: + \u: P x. \p: x =[A] y. =[\x: A. P x] " unfolding lift_def by (derive lems: path_lifting) -schematic_goal lift_comp: +corollary lift_comp: + assumes [intro]: + "P: A \ U i" "A: U i" + "x: A" "u: P x" + shows "lift[A, P, x, x]`u`(refl x) \ refl " +unfolding lift_def apply compute prefer 3 apply compute by derive + +declare + lift_type [intro] + lift_comp [comp] + +text \ +Proof of the computation property of @{const lift}, stating that the first projection of the lift of @{term p} is equal to @{term p}: +\ + +schematic_goal lift_fst_comp: assumes [intro]: "P: A \ U i" "A: U i" "x: A" "y: A" "p: x =[A] y" - "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 + defines + "Fst \ \x y p u. ap[fst[A, P], \x: A. P x, A, , ]" + shows + "?prf: \u: P x. (Fst x y p u)`(lift[A, P, x, y]`u`p) =[x =[A] y] p" +proof + (path_ind' x y p, quantify_all) + fix x assume [intro]: "x: A" + show "\u. u: P x \ + refl(refl x): (Fst x x (refl x) u)`(lift[A, P, x, x]`u`(refl x)) =[x =[A] x] refl x" + unfolding Fst_def by derive + + fix y p assume [intro]: "y: A" "p: x =[A] y" + show "\u: P x. (Fst x y p u)`(lift[A, \a. P a, x, y]`u`p) =[x =[A] y] p: U i" + proof derive + fix u assume [intro]: "u: P x" + have + "fst[A, P]` \ x" "fst[A, P]` \ y" by derive + moreover have + "Fst x y p u: + =[\(x: A). P x] \ + fst[A, P]` =[A] fst[A, P]`" + unfolding Fst_def by derive + ultimately show + "Fst x y p u: =[\(x: A). P x] \ x =[A] y" + by simp + qed routine +qed fact + + +section \Dependent map\ + +schematic_goal dependent_map: + assumes [intro]: + "A: U i" "B: A \ U i" + "f: \x: A. B x" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: transport[A, B, x, y]`p`(f`x) =[B y] f`y" +proof (path_ind' x y p) + show "\x. x: A \ refl (f`x): transport[A, B, x, x]`(refl x)`(f`x) =[B x] f`x" by derive +qed derive + +definition apd :: "[t, t, t \ t, t, t] \ t" ("(apd[_, _, _, _, _])") where +"apd[f, A, B, x, y] \ + \p: x =[A] y. indEq (\x y p. transport[A, B, x, y]`p`(f`x) =[B y] f`y) (\x. refl (f`x)) x y p" + +corollary apd_type: + assumes [intro]: + "A: U i" "B: A \ U i" + "f: \x: A. B x" + "x: A" "y: A" + shows "apd[f, A, B, x, y]: \p: x =[A] y. transport[A, B, x, y]`p`(f`x) =[B y] f`y" +unfolding apd_def by derive + +declare apd_type [intro] end -- cgit v1.2.3