aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Eq.thy22
-rw-r--r--Type_Families.thy109
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
\<close>
-lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv[A, x, y]`p: y =[A] x"
+lemma inv_type: "\<lbrakk>A: U i; x: A; y: A\<rbrakk> \<Longrightarrow> inv[A, x, y]: x =[A] y \<rightarrow> y =[A] x"
unfolding inv_def by derive
lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv[A, a, a]`(refl a) \<equiv> refl a"
@@ -146,8 +146,8 @@ end
\<close>
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 \<rightarrow> y =[A] z \<rightarrow> x =[A] z"
unfolding pathcomp_def by (derive lems: transitivity)
corollary pathcomp_comp:
@@ -278,21 +278,27 @@ in
end
\<close>
-corollary ap_type:
+corollary ap_typ:
+ assumes [intro]:
+ "A: U i" "B: U i" "f: A \<rightarrow> B"
+ "x: A" "y: A"
+ shows "ap[f, A, B, x, y]: x =[A] y \<rightarrow> f`x =[B] f`y"
+unfolding ap_def by routine
+
+corollary ap_app_typ:
assumes [intro]:
"A: U i" "B: U i" "f: A \<rightarrow> 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 \<rightarrow> B" "x: A"
shows "ap[f, A, B, x, x]`(refl x) \<equiv> 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
\<close>
corollary transport_type:
- assumes [intro]: "A: U i" "P: A \<leadsto> U j" "x: A" "y: A" "p: x =[A] y"
- shows "transport[A, P, x, y]`p: P x \<rightarrow> P y"
+ assumes [intro]: "A: U i" "P: A \<leadsto> U j" "x: A" "y: A"
+ shows "transport[A, P, x, y]: x =[A] y \<rightarrow> P x \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> P y] id P y : U j"
by derive
qed
@@ -101,41 +101,108 @@ declare
transport_invr [intro]
+section \<open>Path lifting\<close>
+
schematic_goal path_lifting:
assumes [intro]:
"P: A \<leadsto> U i" "A: U i"
"x: A" "y: A" "p: x =[A] y"
- shows "?prf: \<Prod>u: P x. <x, u> =[\<Sum>x: A. P x] <y, (transport[A, P, x, y]`p)`u>"
+ shows "?prf: \<Prod>u: P x. <x, u> =[\<Sum>x: A. P x] <y, transport[A, P, x, y]`p`u>"
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 \<equiv> u" by derive
- thus "(refl <x, u>): <x, u> =[\<Sum>(x: A). P x] <x, (transport[A, P, x, x]`(refl x))`u>"
+ thus "(refl <x, u>): <x, u> =[\<Sum>(x: A). P x] <x, transport[A, P, x, x]`(refl x)`u>"
proof simp qed routine
qed routine
definition lift :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t" ("(2lift[_, _, _, _])")
where
"lift[A, P, x, y] \<equiv> \<lambda>u: P x. \<lambda>p: x =[A] y. (indEq
- (\<lambda>x y p. \<Prod>u: P x. <x, u> =[\<Sum>(x: A). P x] <y, (transport[A, P, x, y]`p)`u>)
+ (\<lambda>x y p. \<Prod>u: P x. <x, u> =[\<Sum>(x: A). P x] <y, transport[A, P, x, y]`p`u>)
(\<lambda>x. \<lambda>(u: P x). refl <x, u>) x y p)`u"
corollary lift_type:
assumes [intro]:
"P: A \<leadsto> 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, u> =[\<Sum>x: A. P x] <y, (transport[A, P, x, y]`p)`u>"
+ "x: A" "y: A"
+ shows
+ "lift[A, P, x, y]:
+ \<Prod>u: P x. \<Prod>p: x =[A] y. <x, u> =[\<Sum>x: A. P x] <y, transport[A, P, x, y]`p`u>"
unfolding lift_def by (derive lems: path_lifting)
-schematic_goal lift_comp:
+corollary lift_comp:
+ assumes [intro]:
+ "P: A \<leadsto> U i" "A: U i"
+ "x: A" "u: P x"
+ shows "lift[A, P, x, x]`u`(refl x) \<equiv> refl <x, u>"
+unfolding lift_def apply compute prefer 3 apply compute by derive
+
+declare
+ lift_type [intro]
+ lift_comp [comp]
+
+text \<open>
+Proof of the computation property of @{const lift}, stating that the first projection of the lift of @{term p} is equal to @{term p}:
+\<close>
+
+schematic_goal lift_fst_comp:
assumes [intro]:
"P: A \<leadsto> U i" "A: U i"
"x: A" "y: A" "p: x =[A] y"
- "u: P x"
- defines "Fst \<equiv> ap[fst[A, P], \<Sum>x: A. P x, A, <x, u>, <y, (transport[A, P, x, y]`p)`u>]"
- shows "?prf: Fst`(lift[A, P, x, y]`u`p) =[x =[A] y] p"
-proof derive
-oops
+ defines
+ "Fst \<equiv> \<lambda>x y p u. ap[fst[A, P], \<Sum>x: A. P x, A, <x, u>, <y, transport[A, P, x, y]`p`u>]"
+ shows
+ "?prf: \<Prod>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 "\<And>u. u: P x \<Longrightarrow>
+ 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 "\<Prod>u: P x. (Fst x y p u)`(lift[A, \<lambda>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, u> \<equiv> x" "fst[A, P]`<y, transport[A, P, x, y]`p`u> \<equiv> y" by derive
+ moreover have
+ "Fst x y p u:
+ <x, u> =[\<Sum>(x: A). P x] <y, transport[A, P, x, y]`p`u> \<rightarrow>
+ fst[A, P]`<x, u> =[A] fst[A, P]`<y, transport[A, P, x, y]`p`u>"
+ unfolding Fst_def by derive
+ ultimately show
+ "Fst x y p u: <x, u> =[\<Sum>(x: A). P x] <y, transport[A, P, x, y]`p`u> \<rightarrow> x =[A] y"
+ by simp
+ qed routine
+qed fact
+
+
+section \<open>Dependent map\<close>
+
+schematic_goal dependent_map:
+ assumes [intro]:
+ "A: U i" "B: A \<leadsto> U i"
+ "f: \<Prod>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 "\<And>x. x: A \<Longrightarrow> 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 \<Rightarrow> t, t, t] \<Rightarrow> t" ("(apd[_, _, _, _, _])") where
+"apd[f, A, B, x, y] \<equiv>
+ \<lambda>p: x =[A] y. indEq (\<lambda>x y p. transport[A, B, x, y]`p`(f`x) =[B y] f`y) (\<lambda>x. refl (f`x)) x y p"
+
+corollary apd_type:
+ assumes [intro]:
+ "A: U i" "B: A \<leadsto> U i"
+ "f: \<Prod>x: A. B x"
+ "x: A" "y: A"
+ shows "apd[f, A, B, x, y]: \<Prod>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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 17:41:17 +0000