aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-19 11:55:45 +0200
committerJosh Chen2018-09-19 11:55:45 +0200
commitf602cb54b39b3c1bb4f755db09bdeeb2f31a9559 (patch)
tree94a4b3016aebdc8855d6d12a2bd842649b0d3485
parent59a1409b1d15860344e91a4512b60ab8d4368e44 (diff)
proof of associativity of path composition
-rw-r--r--EqualProps.thy89
-rw-r--r--HoTT_Base.thy11
2 files changed, 73 insertions, 27 deletions
diff --git a/EqualProps.thy b/EqualProps.thy
index f7a8d91..847d964 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -22,6 +22,10 @@ unfolding inv_def by (elim Equal_elim) routine
lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (refl a)\<inverse> \<equiv> refl a"
unfolding inv_def by compute routine
+declare
+ inv_type [intro]
+ inv_comp [comp]
+
section \<open>Transitivity of equality/Path composition\<close>
@@ -35,7 +39,7 @@ syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 120)
translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
lemma pathcomp_type:
- assumes "A: U i" and "x: A" "y: A" "z: A"
+ assumes "A: U i" "x: A" "y: A" "z: A"
shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"
unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms)
@@ -63,6 +67,11 @@ unfolding pathcomp_def proof compute
by (routine add: assms)
qed (routine add: assms)
+declare
+ pathcomp_type [intro]
+ pathcomp_trans [intro]
+ pathcomp_comp [comp]
+
section \<open>Higher groupoid structure of types\<close>
@@ -71,54 +80,86 @@ schematic_goal pathcomp_right_id:
shows "?a: p \<bullet> (refl y) =[x =\<^sub>A y] p"
proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) \<comment> \<open>@{method elim} does not seem to work with schematic goals.\<close>
show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
- by (derive lems: assms pathcomp_comp)
-qed (routine add: assms pathcomp_type)
+ by (derive lems: assms)
+qed (routine add: assms)
schematic_goal pathcomp_left_id:
assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
shows "?a: (refl x) \<bullet> p =[x =\<^sub>A y] p"
proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
- by (derive lems: assms pathcomp_comp)
-qed (routine add: assms pathcomp_type)
+ by (derive lems: assms)
+qed (routine add: assms)
schematic_goal pathcomp_left_inv:
assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)"
proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse> \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
- by (derive lems: assms inv_comp pathcomp_comp)
-qed (routine add: assms inv_type pathcomp_type)
+ by (derive lems: assms)
+qed (routine add: assms)
schematic_goal pathcomp_right_inv:
assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)"
proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x)\<inverse> =[x =\<^sub>A x] (refl x)"
- by (derive lems: assms inv_comp pathcomp_comp)
-qed (routine add: assms inv_type pathcomp_type)
+ by (derive lems: assms)
+qed (routine add: assms)
schematic_goal inv_involutive:
assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse>\<inverse> =[x =\<^sub>A x] (refl x)"
- by (derive lems: assms inv_comp)
-qed (routine add: assms inv_type)
-
-schematic_goal pathcomp_assoc:
- assumes
- "A: U(i)"
- "x: A" "y: A" "z: A" "w: A"
- "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
- shows
- "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r"
-proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
- fix x assume "x: A"
- show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r"
- \<comment> \<open>This requires substitution of *propositional* equality. \<close>
- oops
+ by (derive lems: assms)
+qed (routine add: assms)
+text \<open>All of the propositions above have the same proof term, which we abbreviate here.\<close>
+abbreviation \<iota> :: "t \<Rightarrow> t" where "\<iota> p \<equiv> ind\<^sub>= (\<lambda>x. refl (refl x)) p"
+
+text \<open>The next proof has a triply-nested path induction.\<close>
+
+lemma pathcomp_assoc:
+ assumes "A: U i" "x: A" "y: A" "z: A" "w: A"
+ shows "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q) p:
+ \<Prod>p: x =\<^sub>A y. \<Prod>q: y =\<^sub>A z. \<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r"
+proof
+ show "\<And>p. p: x =\<^sub>A y \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q) p:
+ \<Prod>q: y =\<^sub>A z. \<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] p \<bullet> q \<bullet> r"
+ proof (elim Equal_elim)
+ fix x assume 1: "x: A"
+ show "\<^bold>\<lambda>q. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q:
+ \<Prod>q: x =\<^sub>A z. \<Prod>r: z =\<^sub>A w. refl x \<bullet> (q \<bullet> r) =[x =\<^sub>A w] refl x \<bullet> q \<bullet> r"
+ proof
+ show "\<And>q. q: x =\<^sub>A z \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q:
+ \<Prod>r: z =\<^sub>A w. refl x \<bullet> (q \<bullet> r) =[x =\<^sub>A w] refl x \<bullet> q \<bullet> r"
+ proof (elim Equal_elim)
+ fix x assume *: "x: A"
+ show "\<^bold>\<lambda>r. \<iota> r: \<Prod>r: x =\<^sub>A w. refl x \<bullet> (refl x \<bullet> r) =[x =\<^sub>A w] refl x \<bullet> refl x \<bullet> r"
+ proof
+ show "\<And>r. r: x =[A] w \<Longrightarrow> \<iota> r: refl x \<bullet> (refl x \<bullet> r) =[x =[A] w] refl x \<bullet> refl x \<bullet> r"
+ by (elim Equal_elim, derive lems: * assms)
+ qed (routine add: * assms)
+ qed (routine add: 1 assms)
+ qed (routine add: 1 assms)
+
+ text \<open>
+ In the following part @{method derive} fails to obtain the correct subgoals, so we have to prove the statement manually.
+ \<close>
+ fix y p assume 2: "y: A" "p: x =\<^sub>A y"
+ show "\<Prod>q: y =\<^sub>A z. \<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] p \<bullet> q \<bullet> r: U i"
+ proof (routine add: assms)
+ fix q assume 3: "q: y =\<^sub>A z"
+ show "\<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] p \<bullet> q \<bullet> r: U i"
+ proof (routine add: assms)
+ show "\<And>r. r: z =[A] w \<Longrightarrow> p \<bullet> (q \<bullet> r): x =[A] w" and "\<And>r. r: z =[A] w \<Longrightarrow> p \<bullet> q \<bullet> r: x =[A] w"
+ by (routine add: 1 2 3 assms)
+ qed (routine add: 1 assms)
+ qed fact+
+ qed fact+
+qed (routine add: assms)
+
section \<open>Transport\<close>
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 69cc1b1..0b460d9 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -25,9 +25,14 @@ axiomatization
lt :: "[ord, ord] \<Rightarrow> prop" (infix "<" 999) and
leq :: "[ord, ord] \<Rightarrow> prop" (infix "\<le>" 999)
where
- lt_Suc [intro]: "n < (Suc n)" and
- lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
- leq_min [intro]: "O \<le> n"
+ lt_Suc: "n < (Suc n)" and
+ lt_trans: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
+ leq_min: "O \<le> n"
+
+declare
+ lt_Suc [intro!]
+ leq_min [intro!]
+ lt_trans [intro]
section \<open>Judgment\<close>