blob: abb262305ceec89bc4023ae8d531822b57e6d4e3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
(*
Title: EqualProps.thy
Author: Joshua Chen
Date: 2018
Properties of equality
*)
theory EqualProps
imports HoTT_Methods Equal Prod
begin
section \<open>Symmetry of equality/Path inverse\<close>
definition inv :: "t \<Rightarrow> t" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl x) p"
lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =\<^sub>A y\<rbrakk> \<Longrightarrow> p\<inverse>: y =\<^sub>A x"
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
section \<open>Transitivity of equality/Path composition\<close>
text \<open>
Composition function, of type @{term "x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"} polymorphic over @{term A}, @{term x}, @{term y}, and @{term z}.
\<close>
definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
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"
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)
corollary pathcomp_trans:
assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z"
shows "p \<bullet> q: x =\<^sub>A z"
by (routine add: assms pathcomp_type)
lemma pathcomp_comp:
assumes "A: U i" and "a: A"
shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
unfolding pathcomp_def proof compute
show "(ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) (refl a))`(refl a) \<equiv> refl a"
proof compute
show "\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q): a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
by (routine add: assms)
show "(\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q))`(refl a) \<equiv> refl a"
proof compute
show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>x. refl x) q: a =\<^sub>A a" by (routine add: assms)
qed (derive lems: assms)
qed (routine add: assms)
show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) p: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
by (routine add: assms)
qed (routine add: assms)
section \<open>Higher groupoid structure of types\<close>
schematic_goal pathcomp_right_id:
assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
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)
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)
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)
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)
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>
sorry
oops
section \<open>Transport\<close>
definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>_. (\<^bold>\<lambda>x. x)) p"
text \<open>Note that @{term transport} is a polymorphic function in our formulation.\<close>
lemma transport_type: "\<lbrakk>p: x =\<^sub>A y; x: A; y: A; A: U i; P: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> transport p: P x \<rightarrow> P y"
unfolding transport_def by (elim Equal_elim) routine
lemma transport_comp: "\<lbrakk>A: U i; x: A\<rbrakk> \<Longrightarrow> transport (refl x) \<equiv> id"
unfolding transport_def by derive
end
|
