aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2019-03-06 11:42:19 +0100
committerJosh Chen2019-03-06 11:42:19 +0100
commit8f7164976d08446e77a0e1eceaaa01f0ed363e5b (patch)
tree6cbf9e5963e0273e75b12436cf5b3adc2c30b05c
parentfa4c19c5ddce4d1f2d5ad58170e89cb74cb7f7e1 (diff)
Make functions object-level
Diffstat (limited to '')
-rw-r--r--Eq.thy163
-rw-r--r--Projections.thy40
-rw-r--r--Type_Families.thy80
-rw-r--r--Univalence.thy36
4 files changed, 173 insertions, 146 deletions
diff --git a/Eq.thy b/Eq.thy
index 9a7ba47..ca03089 100644
--- a/Eq.thy
+++ b/Eq.thy
@@ -2,7 +2,12 @@
Isabelle/HoTT: Equality
Feb 2019
-Intensional equality, path induction, and proofs of various results.
+Contains:
+* Type definitions for intensional equality
+* Some setup for path induction
+* Basic properties of equality (inv, pathcomp)
+* The higher groupoid structure of types
+* Functoriality of functions (ap)
********)
@@ -71,32 +76,32 @@ section \<open>Properties of equality\<close>
subsection \<open>Symmetry (path inverse)\<close>
-definition inv :: "[t, t, t, t] \<Rightarrow> t"
-where "inv A x y p \<equiv> indEq (\<lambda>x y. &(y =[A] x)) (\<lambda>x. refl x) x y p"
+definition inv :: "[t, t, t] \<Rightarrow> t"
+where "inv A x y \<equiv> \<lambda>p: x =[A] y. indEq (\<lambda>x y. &(y =[A] x)) (\<lambda>x. refl x) x y p"
-syntax "_inv" :: "[t, t, t, t] \<Rightarrow> t" ("(2inv[_, _, _] _)" [0, 0, 0, 1000] 999)
-translations "inv[A, x, y] p" \<rightleftharpoons> "(CONST inv) A x y p"
+syntax "_inv" :: "[t, t, t] \<Rightarrow> t" ("(2inv[_, _, _])" [0, 0, 0] 999)
+translations "inv[A, x, y]" \<rightleftharpoons> "(CONST inv) A x y"
-syntax "_inv'" :: "t \<Rightarrow> t" ("~_" [1000])
+syntax "_inv'" :: "t \<Rightarrow> t" ("inv")
text \<open>Pretty-printing switch for path inverse:\<close>
ML \<open>val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\<close>
print_translation \<open>
-let fun inv_tr' ctxt [A, x, y, p] =
+let fun inv_tr' ctxt [A, x, y] =
if Config.get ctxt pretty_inv
- then Syntax.const @{syntax_const "_inv'"} $ p
- else Syntax.const @{syntax_const "_inv"} $ A $ x $ y $ p
+ then Syntax.const @{syntax_const "_inv'"}
+ else Syntax.const @{syntax_const "_inv"} $ A $ x $ y
in
[(@{const_syntax inv}, inv_tr')]
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; p: x =[A] y\<rbrakk> \<Longrightarrow> inv[A, x, y]`p: 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"
+lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv[A, a, a]`(refl a) \<equiv> refl a"
unfolding inv_def by derive
declare
@@ -114,27 +119,27 @@ by
path_ind "{x, z, _} x =[A] z",
rule Eq_intro, routine add: assms)
-definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t"
+definition pathcomp :: "[t, t, t, t] \<Rightarrow> t"
where
- "pathcomp A x y z p q \<equiv> (indEq
+ "pathcomp A x y z \<equiv> \<lambda>p: x =[A] y. \<lambda>q: y =[A] z. (indEq
(\<lambda>x y. & \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z)
(\<lambda>x. \<lambda>z: A. \<lambda>q: x =[A] z. indEq (\<lambda>x z. & x =[A] z) (\<lambda>x. refl x) x z q)
x y p)`z`q"
syntax "_pathcomp" :: "[t, t, t, t, t, t] \<Rightarrow> t"
- ("(2pathcomp[_, _, _, _] _ _)" [0, 0, 0, 0, 1000, 1000] 999)
-translations "pathcomp[A, x, y, z] p q" \<rightleftharpoons> "(CONST pathcomp) A x y z p q"
+ ("(2pathcomp[_, _, _, _])" [0, 0, 0, 0] 999)
+translations "pathcomp[A, x, y, z]" \<rightleftharpoons> "(CONST pathcomp) A x y z"
-syntax "_pathcomp'" :: "[t, t] \<Rightarrow> t" (infixl "^" 110)
+syntax "_pathcomp'" :: "[t, t] \<Rightarrow> t" ("pathcomp")
ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<close>
\<comment> \<open>Pretty-printing switch for path composition\<close>
print_translation \<open>
-let fun pathcomp_tr' ctxt [A, x, y, z, p, q] =
+let fun pathcomp_tr' ctxt [A, x, y, z] =
if Config.get ctxt pretty_pathcomp
- then Syntax.const @{syntax_const "_pathcomp'"} $ p $ q
- else Syntax.const @{syntax_const "_pathcomp"} $ A $ x $ y $ z $ p $ q
+ then Syntax.const @{syntax_const "_pathcomp'"}
+ else Syntax.const @{syntax_const "_pathcomp"} $ A $ x $ y $ z
in
[(@{const_syntax pathcomp}, pathcomp_tr')]
end
@@ -142,12 +147,12 @@ 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"
+ shows "pathcomp[A, x, y, z]`p`q: x =[A] z"
unfolding pathcomp_def by (derive lems: transitivity)
corollary pathcomp_comp:
assumes [intro]: "A: U i" "a: A"
- shows "pathcomp[A, a, a, a] (refl a) (refl a) \<equiv> refl a"
+ shows "pathcomp[A, a, a, a]`(refl a)`(refl a) \<equiv> refl a"
unfolding pathcomp_def by (derive lems: transitivity)
declare
@@ -159,45 +164,45 @@ section \<open>Higher groupoid structure of types\<close>
schematic_goal pathcomp_idr:
assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?prf: pathcomp[A, x, y, y] p (refl y) =[x =[A] y] p"
+ shows "?prf: pathcomp[A, x, y, y]`p`(refl y) =[x =[A] y] p"
proof (path_ind' x y p)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp[A, x, x, x] (refl x) (refl x) =[x =[A] x] (refl x)"
+ show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp[A, x, x, x]`(refl x)`(refl x) =[x =[A] x] (refl x)"
by derive
qed routine
schematic_goal pathcomp_idl:
assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?prf: pathcomp[A, x, x, y] (refl x) p =[x =[A] y] p"
+ shows "?prf: pathcomp[A, x, x, y]`(refl x)`p =[x =[A] y] p"
proof (path_ind' x y p)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp[A, x, x, x] (refl x) (refl x) =[x =[A] x] (refl x)"
+ show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp[A, x, x, x]`(refl x)`(refl x) =[x =[A] x] (refl x)"
by derive
qed routine
schematic_goal pathcomp_invr:
assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?prf: pathcomp[A, x, y, x] p (inv[A, x, y] p) =[x =[A] x] (refl x)"
+ shows "?prf: pathcomp[A, x, y, x]`p`(inv[A, x, y]`p) =[x =[A] x] (refl x)"
proof (path_ind' x y p)
show
"\<And>x. x: A \<Longrightarrow> refl(refl x):
- pathcomp[A, x, x, x] (refl x) (inv[A, x, x] (refl x)) =[x =[A] x] (refl x)"
+ pathcomp[A, x, x, x]`(refl x)`(inv[A, x, x]`(refl x)) =[x =[A] x] (refl x)"
by derive
qed routine
schematic_goal pathcomp_invl:
assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?prf: pathcomp[A, y, x, y] (inv[A, x, y] p) p =[y =[A] y] refl(y)"
+ shows "?prf: pathcomp[A, y, x, y]`(inv[A, x, y]`p)`p =[y =[A] y] refl(y)"
proof (path_ind' x y p)
show
"\<And>x. x: A \<Longrightarrow> refl(refl x):
- pathcomp[A, x, x, x] (inv[A, x, x] (refl x)) (refl x) =[x =[A] x] (refl x)"
+ pathcomp[A, x, x, x]`(inv[A, x, x]`(refl x))`(refl x) =[x =[A] x] (refl x)"
by derive
qed routine
schematic_goal inv_involutive:
assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?prf: inv[A, y, x] (inv[A, x, y] p) =[x =[A] y] p"
+ shows "?prf: inv[A, y, x]`(inv[A, x, y]`p) =[x =[A] y] p"
proof (path_ind' x y p)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)"
+ show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv[A, x, x]`(inv[A, x, x]`(refl x)) =[x =[A] x] (refl x)"
by derive
qed routine
@@ -215,31 +220,31 @@ schematic_goal pathcomp_assoc:
assumes [intro]: "A: U i"
shows
"?prf: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z. \<Prod>w: A. \<Prod>r: z =[A] w.
- pathcomp[A, x, y, w] p (pathcomp[A, y, z, w] q r) =[x =[A] w]
- pathcomp[A, x, z, w] (pathcomp[A, x, y, z] p q) r"
+ pathcomp[A, x, y, w]`p`(pathcomp[A, y, z, w]`q`r) =[x =[A] w]
+ pathcomp[A, x, z, w]`(pathcomp[A, x, y, z]`p`q)`r"
apply (quantify 3)
apply (path_ind "{x, y, p}
\<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w).
- pathcomp[A, x, y, w] p (pathcomp[A, y, z, w] q r) =[x =[A] w]
- pathcomp[A, x, z, w] (pathcomp[A, x, y, z] p q) r")
+ pathcomp[A, x, y, w]`p`(pathcomp[A, y, z, w]`q`r) =[x =[A] w]
+ pathcomp[A, x, z, w]`(pathcomp[A, x, y, z]`p`q)`r")
apply (quantify 2)
apply (path_ind "{x, z, q}
\<Prod>(w: A). \<Prod>(r: z =[A] w).
- pathcomp[A, x, x, w] (refl x) (pathcomp[A, x, z, w] q r) =[x =[A] w]
- pathcomp[A, x, z, w] (pathcomp[A, x, x, z] (refl x) q) r")
+ pathcomp[A, x, x, w]`(refl x)`(pathcomp[A, x, z, w]`q`r) =[x =[A] w]
+ pathcomp[A, x, z, w]`(pathcomp[A, x, x, z]`(refl x)`q)`r")
apply (quantify 2)
apply (path_ind "{x, w, r}
- pathcomp[A, x, x, w] (refl x) (pathcomp[A, x, x, w] (refl x) r) =[x =[A] w]
- pathcomp[A, x, x, w] (pathcomp[A, x, x, x] (refl x) (refl x)) r")
+ pathcomp[A, x, x, w]`(refl x)`(pathcomp[A, x, x, w] `(refl x)`r) =[x =[A] w]
+ pathcomp[A, x, x, w]`(pathcomp[A, x, x, x]`(refl x)`(refl x))`r")
text \<open>The rest is now routine.\<close>
proof -
show
"\<And>x. x: A \<Longrightarrow> refl(refl x):
- pathcomp[A, x, x, x] (refl x) (pathcomp[A, x, x, x] (refl x) (refl x)) =[x =[A] x]
- pathcomp[A, x, x, x] (pathcomp[A, x, x, x] (refl x) (refl x)) (refl x)"
+ pathcomp[A, x, x, x]`(refl x)`(pathcomp[A, x, x, x]`(refl x)`(refl x)) =[x =[A] x]
+ pathcomp[A, x, x, x]`(pathcomp[A, x, x, x]`(refl x)`(refl x))`(refl x)"
by derive
qed routine
@@ -254,35 +259,35 @@ schematic_goal transfer:
by (path_ind' x y p, rule Eq_routine, routine)
definition ap :: "[t, t, t, t, t] \<Rightarrow> t"
-where "ap B f x y p \<equiv> indEq ({x, y, _} f`x =[B] f`y) (\<lambda>x. refl (f`x)) x y p"
+where "ap f A B x y \<equiv> \<lambda>p: x =[A] y. indEq ({x, y, _} f`x =[B] f`y) (\<lambda>x. refl (f`x)) x y p"
-syntax "_ap" :: "[t, t, t, t, t] \<Rightarrow> t" ("(2ap[_, _, _] _ _)" [0, 0, 0, 1000, 1000])
-translations "ap[B, x, y] f p" \<rightleftharpoons> "(CONST ap) B f x y p"
+syntax "_ap" :: "[t, t, t, t, t] \<Rightarrow> t" ("(2ap[_, _, _, _, _])")
+translations "ap[f, A, B, x, y]" \<rightleftharpoons> "(CONST ap) f A B x y"
-syntax "_ap'" :: "[t, t] \<Rightarrow> t" ("(_{_})" [1000, 0] 1000)
+syntax "_ap'" :: "t \<Rightarrow> t" ("ap[_]")
ML \<open>val pretty_ap = Attrib.setup_config_bool @{binding "pretty_ap"} (K true)\<close>
print_translation \<open>
-let fun ap_tr' ctxt [B, f, x, y, p] =
+let fun ap_tr' ctxt [f, A, B, x, y] =
if Config.get ctxt pretty_ap
- then Syntax.const @{syntax_const "_ap'"} $ f $ p
- else Syntax.const @{syntax_const "_ap"} $ B $ x $ y $ f $ p
+ then Syntax.const @{syntax_const "_ap'"} $ f
+ else Syntax.const @{syntax_const "_ap"} $ f $ A $ B $ x $ y
in
[(@{const_syntax ap}, ap_tr')]
end
\<close>
corollary ap_type:
- assumes
+ assumes [intro]:
"A: U i" "B: U i" "f: A \<rightarrow> B"
"x: A" "y: A" "p: x =[A] y"
- shows "ap[B, x, y] f p: f`x =[B] f`y"
-unfolding ap_def using assms by (rule transfer)
+ shows "ap[f, A, B, x, y]`p: f`x =[B] f`y"
+unfolding ap_def by routine
lemma ap_comp:
assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A"
- shows "ap[B, x, x] f (refl x) \<equiv> refl (f`x)"
+ shows "ap[f, A, B, x, x]`(refl x) \<equiv> refl (f`x)"
unfolding ap_def by derive
declare
@@ -294,22 +299,22 @@ schematic_goal ap_func_pathcomp:
assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B"
shows
"?prf: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z.
- ap[B, x, z] f (pathcomp[A, x, y, z] p q) =[f`x =[B] f`z]
- pathcomp[B, f`x, f`y, f`z] (ap[B, x, y] f p) (ap[B, y, z] f q)"
+ ap[f, A, B, x, z]`(pathcomp[A, x, y, z]`p`q) =[f`x =[B] f`z]
+ pathcomp[B, f`x, f`y, f`z]`(ap[f, A, B, x, y]`p)`(ap[f, A, B, y, z]`q)"
apply (quantify 3)
apply (path_ind "{x, y, p}
\<Prod>z: A. \<Prod>q: y =[A] z.
- ap[B, x, z] f (pathcomp[A, x, y, z] p q) =[f`x =[B] f`z]
- pathcomp[B, f`x, f`y, f`z] (ap[B, x, y] f p) (ap[B, y, z] f q)")
+ ap[f, A, B, x, z]`(pathcomp[A, x, y, z]`p`q) =[f`x =[B] f`z]
+ pathcomp[B, f`x, f`y, f`z]`(ap[f, A, B, x, y]`p)`(ap[f, A, B, y, z]`q)")
apply (quantify 2)
apply (path_ind "{x, z, q}
- ap[B, x, z] f (pathcomp[A, x, x, z] (refl x) q) =[f`x =[B] f`z]
- pathcomp[B, f`x, f`x, f`z] (ap[B, x, x] f (refl x)) (ap[B, x, z] f q)")
+ ap[f, A, B, x, z]`(pathcomp[A, x, x, z]`(refl x)`q) =[f`x =[B] f`z]
+ pathcomp[B, f`x, f`x, f`z]`(ap[f, A, B, x, x]`(refl x))`(ap[f, A, B, x, z]`q)")
proof -
show
"\<And>x. x: A \<Longrightarrow> refl(refl(f`x)) :
- ap[B, x, x] f (pathcomp[A, x, x, x] (refl x) (refl x)) =[f`x =[B] f`x]
- pathcomp[B, f`x, f`x, f`x] (ap[B, x, x] f (refl x)) (ap[B, x, x] f (refl x))"
+ ap[f, A, B, x, x]`(pathcomp[A, x, x, x]`(refl x)`(refl x)) =[f`x =[B] f`x]
+ pathcomp[B, f`x, f`x, f`x]`(ap[f, A, B, x, x]`(refl x))`(ap[f, A, B, x, x]`(refl x))"
by derive
qed routine
@@ -320,55 +325,59 @@ schematic_goal ap_func_compose:
"f: A \<rightarrow> B" "g: B \<rightarrow> C"
shows
"?prf: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y.
- ap[C, f`x, f`y] g (ap[B, x, y] f p) =[g`(f`x) =[C] g`(f`y)]
- ap[C, x, y] (g o[A] f) p"
+ ap[g, B, C, f`x, f`y]`(ap[f, A, B, x, y]`p) =[g`(f`x) =[C] g`(f`y)]
+ ap[g o[A] f, A, C, x, y]`p"
apply (quantify 3)
apply (path_ind "{x, y, p}
- ap[C, f`x, f`y] g (ap[B, x, y] f p) =[g`(f`x) =[C] g`(f`y)]
- ap[C, x, y] (g o[A] f) p")
+ ap[g, B, C, f`x, f`y]`(ap[f, A, B, x, y]`p) =[g`(f`x) =[C] g`(f`y)]
+ ap[g o[A] f, A, C, x, y]`p")
proof -
show "\<And>x. x: A \<Longrightarrow> refl(refl (g`(f`x))) :
- ap[C, f`x, f`x] g (ap[B, x, x] f (refl x)) =[g`(f`x) =[C] g`(f`x)]
- ap[C, x, x] (g o[A] f) (refl x)"
+ ap[g, B, C, f`x, f`x]`(ap[f, A, B, x, x]`(refl x)) =[g`(f`x) =[C] g`(f`x)]
+ ap[g o[A] f, A, C, x, x]`(refl x)"
unfolding compose_def by derive
fix x y p assume [intro]: "x: A" "y: A" "p: x =[A] y"
- show "ap[C, f`x, f`y] g (ap[B, x, y] f p) =[g`(f`x) =[C] g`(f`y)] ap[C, x, y] (g o[A] f) p: U i"
+ show
+ "ap[g, B, C, f`x, f`y]`(ap[f, A, B, x, y]`p) =[g`(f`x) =[C] g`(f`y)]
+ ap[g o[A] f, A, C, x, y]`p: U i"
proof
have
- "ap[C, x, y] (g o[A] f) p: (\<lambda>x: A. g`(f`x))`x =[C] (\<lambda>x: A. g`(f`x))`y"
+ "ap[g o[A] f, A, C, x, y]`p: (\<lambda>x: A. g`(f`x))`x =[C] (\<lambda>x: A. g`(f`x))`y"
unfolding compose_def by derive
moreover have
"(\<lambda>x: A. g`(f`x))`x =[C] (\<lambda>x: A. g`(f`x))`y \<equiv> g`(f`x) =[C] g`(f`y)" by derive
ultimately show
- "ap[C, x, y] (g o[A] f) p: g`(f`x) =[C] g`(f`y)" by simp
+ "ap[g o[A] f, A, C, x, y]`p: g`(f`x) =[C] g`(f`y)" by simp
qed derive
qed routine
-declare[[pretty_inv=false, pretty_ap=false]]
+
schematic_goal ap_func_inv:
assumes [intro]:
"A: U i" "B: U i" "f: A \<rightarrow> B"
"x: A" "y: A" "p: x =[A] y"
- shows "?prf: ap[B, y, x] f (inv[A, x, y] p) =[f`y =[B] f`x] inv[B, f`x, f`y] (ap[B, x, y] f p)"
+ shows "?prf:
+ ap[f, A, B, y, x]`(inv[A, x, y]`p) =[f`y =[B] f`x] inv[B, f`x, f`y]`(ap[f, A, B, x, y]`p)"
proof (path_ind' x y p)
show "\<And>x. x: A \<Longrightarrow> refl(refl(f`x)):
- ap[B, x, x] f (inv[A, x, x] (refl x)) =[f`x =[B] f`x] inv[B, f`x, f`x] (ap[B, x, x] f (refl x))"
+ ap[f, A, B, x, x]`(inv[A, x, x]`(refl x)) =[f`x =[B] f`x]
+ inv[B, f`x, f`x]`(ap[f, A, B, x, x]`(refl x))"
by derive
qed routine
schematic_goal ap_func_id:
assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?prf: ap A (id A) x y p =[x =[A] y] p"
+ shows "?prf: ap[id A, A, A, x, y]`p =[x =[A] y] p"
proof (path_ind' x y p)
fix x assume [intro]: "x: A"
- show "refl(refl x): ap[A, x, x] (id A) (refl x) =[x =[A] x] refl x" by derive
+ show "refl(refl x): ap[id A, A, A, x, x]`(refl x) =[x =[A] x] refl x" by derive
fix y p assume [intro]: "y: A" "p: x =[A] y"
- have "ap[A, x, y] (id A) p: (id A)`x =[A] (id A)`y" by derive
+ have "ap[id A, A, A, x, y]`p: (id A)`x =[A] (id A)`y" by derive
moreover have "(id A)`x =[A] (id A)`y \<equiv> x =[A] y" by derive
- ultimately have [intro]: "ap[A, x, y] (id A) p: x =[A] y" by simp
+ ultimately have [intro]: "ap[id A, A, A, x, y]`p: x =[A] y" by simp
- show "ap[A, x, y] (id A) p =[x =[A] y] p: U i" by derive
+ show "ap[id A, A, A, x, y]`p =[x =[A] y] p: U i" by derive
qed
diff --git a/Projections.thy b/Projections.thy
index 1473e08..9eeb57f 100644
--- a/Projections.thy
+++ b/Projections.thy
@@ -11,35 +11,33 @@ imports HoTT_Methods Prod Sum
begin
-definition fst :: "[t, t] \<Rightarrow> t" where "fst A p \<equiv> indSum (\<lambda>_. A) (\<lambda>x y. x) p"
+definition fst ("(2fst[_, _])")
+where "fst[A, B] \<equiv> \<lambda>(p: \<Sum>x: A. B x). indSum (\<lambda>_. A) (\<lambda>x y. x) p"
-lemma fst_type:
- assumes "A: U i" and "p: \<Sum>x: A. B x" shows "fst A p: A"
-unfolding fst_def by (derive lems: assms)
+definition snd ("(2snd[_, _])")
+where "snd[A, B] \<equiv> \<lambda>(p: \<Sum>x: A. B x). indSum (\<lambda>p. B (fst[A, B]`p)) (\<lambda>x y. y) p"
-declare fst_type [intro]
+lemma fst_type:
+ assumes [intro]: "A: U i" "B: A \<leadsto> U i"
+ shows "fst[A, B]: (\<Sum>x: A. B x) \<rightarrow> A"
+unfolding fst_def by derive
lemma fst_cmp:
- assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "fst A <a, b> \<equiv> a"
-unfolding fst_def by (subst comp) (derive lems: assms)
-
-declare fst_cmp [comp]
-
-definition snd :: "[t, t \<Rightarrow> t, t] \<Rightarrow> t" where "snd A B p \<equiv> indSum (\<lambda>p. B (fst A p)) (\<lambda>x y. y) p"
+ assumes [intro]: "A: U i" "B: A \<leadsto> U i" "a: A" "b: B a"
+ shows "fst[A, B]`<a, b> \<equiv> a"
+unfolding fst_def by derive
lemma snd_type:
- assumes "A: U i" and "B: A \<leadsto> U i" and "p: \<Sum>x: A. B x" shows "snd A B p: B (fst A p)"
-unfolding snd_def proof (routine add: assms)
- fix x y assume "x: A" and "y: B x"
- with assms have [comp]: "fst A <x, y> \<equiv> x" by derive
- note \<open>y: B x\<close> then show "y: B (fst A <x, y>)" by compute
-qed
+ assumes [intro]: "A: U i" "B: A \<leadsto> U i"
+ shows "snd[A, B]: \<Prod>(p: \<Sum>x: A. B x). B (fst[A,B]`p)"
+unfolding snd_def by (derive lems: fst_type comp: fst_cmp)
lemma snd_cmp:
- assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "snd A B <a,b> \<equiv> b"
-unfolding snd_def by (derive lems: assms)
+ assumes [intro]: "A: U i" "B: A \<leadsto> U i" "a: A" "b: B a"
+ shows "snd[A, B]`<a, b> \<equiv> b"
+unfolding snd_def proof derive qed (derive lems: assms fst_type comp: fst_cmp)
-lemmas Proj_type [intro] = fst_type snd_type
-lemmas Proj_comp [comp] = fst_cmp snd_cmp
+lemmas proj_type [intro] = fst_type snd_type
+lemmas proj_comp [comp] = fst_cmp snd_cmp
end
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 "\<And>x. x: A \<Longrightarrow> id P x: P x \<rightarrow> P x" by derive
qed routine
-definition transport :: "[t \<Rightarrow> t, t, t, t] \<Rightarrow> t" ("(2transport[_, _, _] _)" [0, 0, 0, 1000])
-where "transport[P, x, y] p \<equiv> indEq (\<lambda>a b. & (P a \<rightarrow> P b)) (\<lambda>x. id P x) x y p"
+definition transport :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t" ("(2transport[_, _, _, _])")
+where "transport[A, P, x, y] \<equiv> \<lambda>p: x =[A] y. indEq (\<lambda>a b. & (P a \<rightarrow> P b)) (\<lambda>x. id P x) x y p"
-syntax "_transport'" :: "[t, t] \<Rightarrow> t" ("(2_*)" [1000])
+syntax "_transport'" :: "t \<Rightarrow> t" ("transport[_]")
ML \<open>val pretty_transport = Attrib.setup_config_bool @{binding "pretty_transport"} (K true)\<close>
print_translation \<open>
-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
\<close>
corollary transport_type:
- assumes "A: U i" "P: A \<leadsto> U j" "x: A" "y: A" "p: x =[A] y"
- shows "transport[P, x, y] p: P x \<rightarrow> P y"
-unfolding transport_def using assms by (rule transport)
+ 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"
+unfolding transport_def by derive
lemma transport_comp:
assumes [intro]: "A: U i" "P: A \<leadsto> U j" "a: A"
- shows "transport P a a (refl a) \<equiv> id P a"
+ shows "transport[A, P, a, a]`(refl a) \<equiv> id P a"
unfolding transport_def by derive
declare
@@ -56,59 +56,85 @@ declare
schematic_goal transport_invl:
assumes [intro]:
- "P: A \<leadsto> U j" "A: U i"
+ "A: U i" "P: A \<leadsto> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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[P, y, x] (inv[A, x, y] p) o[P x] transport[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
schematic_goal transport_invr:
assumes [intro]:
- "P: A \<leadsto> U j" "A: U i"
+ "A: U i" "P: A \<leadsto> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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 \<rightarrow> 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 \<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
-(* The two proofs above are rather brittle: the assumption "P: A \<leadsto> 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 \<leadsto> U j"
+ 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>"
+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>"
+ 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. \<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>"
+unfolding lift_def by (derive lems: path_lifting)
+
+schematic_goal lift_comp:
+ assumes [intro]:
+ "P: A \<leadsto> U i" "A: U i"
"x: A" "y: A" "p: x =[A] y"
- shows "?prf: <x, u> =[\<Sum>x: A. P x] <y, (transport[P, x, y] p)`u>"
+ "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
diff --git a/Univalence.thy b/Univalence.thy
index 30110f1..322dbbd 100644
--- a/Univalence.thy
+++ b/Univalence.thy
@@ -117,22 +117,16 @@ schematic_goal transport_invl_hom:
"P: A \<leadsto> U j" "A: U i"
"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) ~[w: P x. P x] id P x"
-proof (rule happly_type[OF transport_invl])
- show "(transport[P, y, x] (inv[A, x, y] p)) o[P x] (transport[P, x, y] p): P x \<rightarrow> P x"
- proof show "P y: U j" by routine qed routine
-qed routine
+ (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]:
- "P: A \<leadsto> U j" "A: U i"
- "x: A" "y: A" "p: x =[A] y"
+ "A: U i" "P: A \<leadsto> U j"
+ "y: A" "x: A" "p: x =[A] y"
shows "?prf:
- (transport[P, x, y] p) o[P y] (transport[P, y, x] (inv[A, x, y] p)) ~[w: P y. P y] id P y"
-proof (rule happly_type[OF transport_invr])
- show "(transport[P, x, y] p) o[P y] (transport[P, y, x] (inv[A, x, y] p)): P y \<rightarrow> P y"
- proof show "P x: U j" by routine qed routine
-qed routine
+ (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]
@@ -145,7 +139,7 @@ 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[Id, A, B] p)"
+ shows "?prf: biinv[A, B] (transport[U i, Id, A, B]`p)"
unfolding biinv_def
apply (rule Sum_routine)
prefer 2
@@ -173,25 +167,25 @@ done
*)
definition idtoeqv :: "[ord, t, t] \<Rightarrow> t" ("(2idtoeqv[_, _, _])") where "
idtoeqv[i, A, B] \<equiv>
- \<lambda>(p: A =[U i] B).
- < transport (Id) A B p, <
- < transport[Id, B, A] (inv[U i, A, B] p),
+ \<lambda>p: A =[U i] B.
+ < transport[U i, Id, A, B]`p, <
+ < transport[U i, Id, B, A]`(inv[U i, A, B]`p),
happly[x: A. A]
- ((transport[Id, B, A] (inv[U i, A, B] p)) o[A] transport[Id, A, B] p)
+ ((transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p)
(id A)
(indEq
(\<lambda>A B p.
- (transport[Id, B, A] (inv[U i, A, B] p)) o[A] transport[Id, A, B] p
+ (transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p
=[A \<rightarrow> A] id A)
(\<lambda>x. refl (id x)) A B p)
>,
- < transport (Id) B A (inv[U i, A, B] p),
+ < transport[U i, Id, B, A]`(inv[U i, A, B]`p),
happly[x: B. B]
- ((transport[Id, A, B] p) o[B] (transport[Id, B, A] (inv[U i, A, B] p)))
+ ((transport[U i, Id, A, B]`p) o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p)))
(id B)
(indEq
(\<lambda>A B p.
- transport[Id, A, B] p o[B] (transport[Id, B, A] (inv[U i, A, B] p))
+ transport[U i, Id, A, B]`p o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p))
=[B \<rightarrow> B] id B)
(\<lambda>x. refl (id x)) A B p)
>