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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
(* Title: HoTT/Univalence.thy
Author: Joshua Chen
Definitions of homotopy, equivalence and the univalence axiom.
*)
theory Univalence
imports
HoTT_Methods
EqualProps
ProdProps
Sum
begin
section \<open>Homotopy and equivalence\<close>
axiomatization homotopic :: "[t, t] \<Rightarrow> t" (infix "~" 100) where
homotopic_def: "\<lbrakk>
f: \<Prod>x:A. B x;
g: \<Prod>x:A. B x
\<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"
axiomatization isequiv :: "t \<Rightarrow> t" where
isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)"
definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<simeq>" 100)
where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f"
text "The identity function is an equivalence:"
lemma isequiv_id:
assumes "A: U i" and "id: A \<rightarrow> A"
shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id"
proof (derive lems: assms isequiv_def homotopic_def)
fix g assume asm: "g: A \<rightarrow> A"
show "id \<circ> g: A \<rightarrow> A"
unfolding compose_def by (routine lems: asm assms)
show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i"
unfolding compose_def by (routine lems: asm assms)
next
show "<\<^bold>\<lambda>x. x, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~ id"
unfolding compose_def by (derive lems: assms homotopic_def)
show "<\<^bold>\<lambda>x. x, lambda refl>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~ id"
unfolding compose_def by (derive lems: assms homotopic_def)
qed (rule assms)
text "We use the following lemma in a few proofs:"
lemma isequiv_type:
assumes "A: U i" and "B: U i" and "f: A \<rightarrow> B"
shows "isequiv f: U i"
by (derive lems: assms isequiv_def homotopic_def compose_def)
text "The equivalence relation \<open>\<simeq>\<close> is symmetric:"
lemma equiv_sym:
assumes "A: U i" and "id: A \<rightarrow> A"
shows "<id, <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>>: A \<simeq> A"
unfolding equivalence_def proof
show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" using assms by (rule isequiv_id)
fix f assume "f: A \<rightarrow> A"
with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type)
qed (rule assms)
section \<open>idtoeqv and the univalence axiom\<close>
definition idtoeqv :: t
where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"
text "We prove that equal types are equivalent. The proof is long and uses universes."
theorem
assumes "A: U i" and "B: U i"
shows "idtoeqv: (A =[U i] B) \<rightarrow> A \<simeq> B"
unfolding idtoeqv_def equivalence_def
proof
fix p assume "p: A =[U i] B"
show "<transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>: \<Sum>f: A \<rightarrow> B. isequiv f"
proof
{ fix f assume "f: A \<rightarrow> B"
with assms show "isequiv f: U i" by (rule isequiv_type)
}
show "transport p: A \<rightarrow> B"
proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="Suc i"])
show "\<And>x. x: U i \<Longrightarrow> x: U (Suc i)" by cumulativity
show "U i: U (Suc i)" by hierarchy
qed fact+
show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)"
proof (rule Equal_elim[where ?C="\<lambda>_ _ p. isequiv (transport p)"])
fix A assume asm: "A: U i"
show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv (transport (refl A))"
proof (derive lems: isequiv_def)
show "transport (refl A): A \<rightarrow> A"
unfolding transport_def
by (compute lems: Equal_comp[where ?A="U i" and ?C="\<lambda>_ _ _. A \<rightarrow> A"]) (derive lems: asm)
show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
(\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times>
(\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)"
proof (subst (1 2) transport_comp)
show "U i: U (Suc i)" by (rule U_hierarchy) rule
show "U i: U (Suc i)" by (rule U_hierarchy) rule
show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
(\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)"
proof
show "\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id: U i"
proof (derive lems: asm homotopic_def)
fix g assume asm': "g: A \<rightarrow> A"
show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
qed (routine lems: asm)
show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. id \<circ> g ~ id"
proof
fix g assume asm': "g: A \<rightarrow> A"
show "id \<circ> g ~ id: U i"
proof (derive lems: homotopic_def)
show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
qed (routine lems: asm)
next
show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
proof compute
show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
qed (rule asm)
qed (routine lems: asm)
show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. g \<circ> id ~ id"
proof
fix g assume asm': "g: A \<rightarrow> A"
show "g \<circ> id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def)
next
show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
proof compute
show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
qed (rule asm)
qed (routine lems: asm)
qed
qed fact+
qed
next
fix A' B' p' assume asm: "A': U i" "B': U i" "p': A' =[U i] B'"
show "isequiv (transport p'): U i"
proof (rule isequiv_type)
show "transport p': A' \<rightarrow> B'" by (derive lems: asm transport_def)
qed fact+
qed fact+
qed
next
show "A =[U i] B: U (Suc i)" proof (derive lems: assms, (rule U_hierarchy, rule lt_Suc)?)+
qed
text "The univalence axiom."
axiomatization univalence :: t where
UA: "univalence: isequiv idtoeqv"
end
|
