aboutsummaryrefslogtreecommitdiff
path: root/hott/Equivalence.thy
blob: d9766777c300a18a97b70b1e57108c1c11b7eeb6 (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
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
theory Equivalence
imports Identity

begin

section \<open>Homotopy\<close>

definition "homotopy A B f g \<equiv> \<Prod>x: A. f `x =\<^bsub>B x\<^esub> g `x"

definition homotopy_i (infix "~" 100)
  where [implicit]: "f ~ g \<equiv> homotopy ? ? f g"

translations "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"

Lemma homotopy_type [typechk]:
  assumes
    "A: U i"
    "\<And>x. x: A \<Longrightarrow> B x: U i"
    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
  shows "f ~ g: U i"
  unfolding homotopy_def by typechk

Lemma (derive) homotopy_refl [refl]:
  assumes
    "A: U i"
    "f: \<Prod>x: A. B x"
  shows "f ~ f"
  unfolding homotopy_def by intros

Lemma (derive) hsym:
  assumes
    "f: \<Prod>x: A. B x"
    "g: \<Prod>x: A. B x"
    "A: U i"
    "\<And>x. x: A \<Longrightarrow> B x: U i"
  shows "H: f ~ g \<Longrightarrow> g ~ f"
  unfolding homotopy_def
  apply intro
    apply (rule pathinv)
      \<guillemotright> by (elim H)
      \<guillemotright> by typechk
  done

Lemma (derive) htrans:
  assumes
    "f: \<Prod>x: A. B x"
    "g: \<Prod>x: A. B x"
    "h: \<Prod>x: A. B x"
    "A: U i"
    "\<And>x. x: A \<Longrightarrow> B x: U i"
  shows "\<lbrakk>H1: f ~ g; H2: g ~ h\<rbrakk> \<Longrightarrow> f ~ h"
  unfolding homotopy_def
  apply intro
    \<guillemotright> vars x
      apply (rule pathcomp[where ?y="g x"])
        \<^item> by (elim H1)
        \<^item> by (elim H2)
      done
    \<guillemotright> by typechk
  done

text \<open>For calculations:\<close>

congruence "f ~ g" rhs g

lemmas
  homotopy_sym [sym] = hsym[rotated 4] and
  homotopy_trans [trans] = htrans[rotated 5]

Lemma (derive) commute_homotopy:
  assumes
    "A: U i" "B: U i"
    "x: A" "y: A"
    "p: x =\<^bsub>A\<^esub> y"
    "f: A \<rightarrow> B" "g: A \<rightarrow> B"
    "H: homotopy A (fn _. B) f g"
  shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
  \<comment> \<open>Need this assumption unfolded for typechecking\<close>
  supply assms(8)[unfolded homotopy_def]
  apply (eq p)
    focus vars x
      apply reduce
        \<comment> \<open>Here it would really be nice to have automation for transport and
          propositional equality.\<close>
        apply (rule use_transport[where ?y="H x \<bullet> refl (g x)"])
          \<guillemotright> by (rule pathcomp_refl)
          \<guillemotright> by (rule pathinv) (rule refl_pathcomp)
          \<guillemotright> by typechk
    done
  done

Corollary (derive) commute_homotopy':
  assumes
    "A: U i"
    "x: A"
    "f: A \<rightarrow> A"
    "H: homotopy A (fn _. A) f (id A)"
  shows "H (f x) = f [H x]"
oops

Lemma homotopy_id_left [typechk]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "homotopy_refl A f: (id B) \<circ> f ~ f"
  unfolding homotopy_refl_def homotopy_def by reduce

Lemma homotopy_id_right [typechk]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "homotopy_refl A f: f \<circ> (id A) ~ f"
  unfolding homotopy_refl_def homotopy_def
 by reduce

Lemma homotopy_funcomp_left:
  assumes
    "H: homotopy B C g g'"
    "f: A \<rightarrow> B"
    "g: \<Prod>x: B. C x"
    "g': \<Prod>x: B. C x"
    "A: U i" "B: U i"
    "\<And>x. x: B \<Longrightarrow> C x: U i"
  shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g' \<circ>\<^bsub>A\<^esub> f)"
  unfolding homotopy_def
  apply (intro; reduce)
    apply (insert \<open>H: _\<close>[unfolded homotopy_def])
      apply (elim H)
  done

Lemma homotopy_funcomp_right:
  assumes
    "H: homotopy A (fn _. B) f f'"
    "f: A \<rightarrow> B"
    "f': A \<rightarrow> B"
    "g: B \<rightarrow> C"
    "A: U i" "B: U i" "C: U i"
  shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g \<circ>\<^bsub>A\<^esub> f')"
  unfolding homotopy_def
  apply (intro; reduce)
    apply (insert \<open>H: _\<close>[unfolded homotopy_def])
      apply (dest PiE, assumption)
      apply (rule ap, assumption)
  done

method id_htpy = (rule homotopy_id_left)
method htpy_id = (rule homotopy_id_right)
method htpy_o = (rule homotopy_funcomp_left)
method o_htpy = (rule homotopy_funcomp_right)


section \<open>Quasi-inverse and bi-invertibility\<close>

subsection \<open>Quasi-inverses\<close>

definition "qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
  homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)"

lemma qinv_type [typechk]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "qinv A B f: U i"
  unfolding qinv_def by typechk

definition qinv_i ("qinv")
  where [implicit]: "qinv f \<equiv> Equivalence.qinv ? ? f"

translations "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f"

Lemma (derive) id_qinv:
  assumes "A: U i"
  shows "qinv (id A)"
  unfolding qinv_def
  proof intro
    show "id A: A \<rightarrow> A" by typechk
  qed (reduce, intro; refl)

Lemma (derive) quasiinv_qinv:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "prf: qinv f \<Longrightarrow> qinv (fst prf)"
  unfolding qinv_def
  apply intro
  \<guillemotright> by (rule \<open>f:_\<close>)
  \<guillemotright> apply (elim "prf")
    focus vars g HH
      apply intro
        \<^item> by reduce (snd HH)
        \<^item> by reduce (fst HH)
    done
    done
  done

Lemma (derive) funcomp_qinv:
  assumes
    "A: U i" "B: U i" "C: U i"
    "f: A \<rightarrow> B" "g: B \<rightarrow> C"
  shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)"
  apply (intros, unfold qinv_def, elims)
  focus prems vars _ _ finv _ ginv
    apply (intro, rule funcompI[where ?f=ginv and ?g=finv])
    proof (reduce, intro)
      have "finv \<circ> ginv \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl
      also have ".. ~ finv \<circ> id B \<circ> f" by (o_htpy, htpy_o) fact
      also have ".. ~ id A" by reduce fact
      finally show "finv \<circ> ginv \<circ> g \<circ> f ~ id A" by this

      have "g \<circ> f \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl
      also have ".. ~ g \<circ> id B \<circ> ginv" by (o_htpy, htpy_o) fact
      also have ".. ~ id C" by reduce fact
      finally show "g \<circ> f \<circ> finv \<circ> ginv ~ id C" by this
    qed
  done

subsection \<open>Bi-invertible maps\<close>

definition "biinv A B f \<equiv>
  (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
    \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"

lemma biinv_type [typechk]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "biinv A B f: U i"
  unfolding biinv_def by typechk

definition biinv_i ("biinv")
  where [implicit]: "biinv f \<equiv> Equivalence.biinv ? ? f"

translations "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f"

Lemma (derive) qinv_imp_biinv:
  assumes
    "A: U i" "B: U i"
    "f: A \<rightarrow> B"
  shows "?prf: qinv f \<rightarrow> biinv f"
  apply intros
  unfolding qinv_def biinv_def
  by (rule Sig_dist_exp)

text \<open>
  Show that bi-invertible maps are quasi-inverses, as a demonstration of how to
  work in this system.
\<close>

Lemma (derive) biinv_imp_qinv:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "biinv f \<rightarrow> qinv f"

  text \<open>Split the hypothesis \<^term>\<open>biinv f\<close> into its components:\<close>
  apply intro
  unfolding biinv_def
  apply elims

  text \<open>Name the components:\<close>
  focus prems vars _ _ _ g H1 h H2
  thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close>

  text \<open>
    \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>, so the proof will be a triple
    \<^term>\<open><g, <?H1, ?H2>>\<close>.
  \<close>
  unfolding qinv_def
  apply intro
    \<guillemotright> by (fact \<open>g: _\<close>)
    \<guillemotright> apply intro
      text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close>
      apply (fact \<open>H1: _\<close>)

      text \<open>
        It remains to prove \<^prop>\<open>?H2: f \<circ> g ~ id B\<close>. First show that \<open>g ~ h\<close>,
        then the result follows from @{thm \<open>H2: f \<circ> h ~ id B\<close>}. Here a proof
        block is used to calculate "forward".
      \<close>
      proof -
        have "g ~ g \<circ> (id B)" by reduce refl
        also have ".. ~ g \<circ> f \<circ> h" by o_htpy (rule \<open>H2:_\<close>[symmetric])
        also have ".. ~ (id A) \<circ> h" by (subst funcomp_assoc[symmetric]) (htpy_o, fact)
        also have ".. ~ h" by reduce refl
        finally have "g ~ h" by this
        then have "f \<circ> g ~ f \<circ> h" by (o_htpy, this)
        also note \<open>H2:_\<close>
        finally show "f \<circ> g ~ id B" by this
      qed
    done
  done

Lemma (derive) id_biinv:
  "A: U i \<Longrightarrow> biinv (id A)"
  by (rule qinv_imp_biinv) (rule id_qinv)

Lemma (derive) funcomp_biinv:
  assumes
    "A: U i" "B: U i" "C: U i"
    "f: A \<rightarrow> B" "g: B \<rightarrow> C"
  shows "biinv f \<rightarrow> biinv g \<rightarrow> biinv (g \<circ> f)"
  apply intros
  focus vars biinv\<^sub>f biinv\<^sub>g
    by (rule qinv_imp_biinv) (rule funcomp_qinv; rule biinv_imp_qinv)
  done


section \<open>Equivalence\<close>

text \<open>
  Following the HoTT book, we first define equivalence in terms of
  bi-invertibility.
\<close>

definition equivalence (infix "\<simeq>" 110)
  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.biinv A B f"

lemma equivalence_type [typechk]:
  assumes "A: U i" "B: U i"
  shows "A \<simeq> B: U i"
  unfolding equivalence_def by typechk

Lemma (derive) equivalence_refl:
  assumes "A: U i"
  shows "A \<simeq> A"
  unfolding equivalence_def
  proof intro
    show "biinv (id A)" by (rule qinv_imp_biinv) (rule id_qinv)
  qed typechk

text \<open>
  The following could perhaps be easier with transport (but then I think we need
  univalence?)...
\<close>

Lemma (derive) equivalence_symmetric:
  assumes "A: U i" "B: U i"
  shows "A \<simeq> B \<rightarrow> B \<simeq> A"
  apply intros
  unfolding equivalence_def
  apply elim
  \<guillemotright> vars _ f "prf"
    apply (dest (4) biinv_imp_qinv)
    apply intro
      \<^item> unfolding qinv_def by (rule fst[of "(biinv_imp_qinv A B f) prf"])
      \<^item> by (rule qinv_imp_biinv) (rule quasiinv_qinv)
    done
  done

Lemma (derive) equivalence_transitive:
  assumes "A: U i" "B: U i" "C: U i"
  shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C"
  proof intros
    fix AB BC assume *: "AB: A \<simeq> B" "BC: B \<simeq> C"
    then have
      "fst AB: A \<rightarrow> B" and 1: "snd AB: biinv (fst AB)"
      "fst BC: B \<rightarrow> C" and 2: "snd BC: biinv (fst BC)"
      unfolding equivalence_def by typechk+
    then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk
    moreover have "biinv (fst BC \<circ> fst AB)"
      using * unfolding equivalence_def by (rules funcomp_biinv 1 2)
    ultimately show "A \<simeq> C"
      unfolding equivalence_def by intro facts
  qed

text \<open>
  Equal types are equivalent. We give two proofs: the first by induction, and
  the second by following the HoTT book and showing that transport is an
  equivalence.
\<close>

Lemma
  assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
  shows "A \<simeq> B"
  by (eq p) (rule equivalence_refl)

text \<open>
  The following proof is wordy because (1) the typechecker doesn't rewrite, and
  (2) we don't yet have universe automation.
\<close>

Lemma (derive) id_imp_equiv:
  assumes
    "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
  shows "<trans (id (U i)) p, ?isequiv>: A \<simeq> B"
  unfolding equivalence_def
  apply intros defer
    \<guillemotright> apply (eq p)
      \<^item> prems vars A B
        apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
        using [[solve_side_conds=1]]
        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
        apply (rule transport, rule Ui_in_USi)
        apply (rule lift_universe_codomain, rule Ui_in_USi)
        apply (typechk, rule Ui_in_USi)
        done
      \<^item> prems vars A
        using [[solve_side_conds=1]]
        apply (subst transport_comp)
          \<^enum> by (rule Ui_in_USi)
          \<^enum> by reduce (rule in_USi_if_in_Ui)
          \<^enum> by reduce (rule id_biinv)
        done
      done

    \<guillemotright> \<comment> \<open>Similar proof as in the first subgoal above\<close>
      apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
      using [[solve_side_conds=1]]
      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
      apply (rule transport, rule Ui_in_USi)
      apply (rule lift_universe_codomain, rule Ui_in_USi)
      apply (typechk, rule Ui_in_USi)
      done
  done

(*Uncomment this to see all implicits from here on.
no_translations
  "f x" \<leftharpoondown> "f `x"
  "x = y" \<leftharpoondown> "x =\<^bsub>A\<^esub> y"
  "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
  "p\<inverse>" \<leftharpoondown> "CONST pathinv A x y p"
  "p \<bullet> q" \<leftharpoondown> "CONST pathcomp A x y z p q"
  "fst" \<leftharpoondown> "CONST Spartan.fst A B"
  "snd" \<leftharpoondown> "CONST Spartan.snd A B"
  "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
  "trans P p" \<leftharpoondown> "CONST transport A P x y p"
  "trans_const B p" \<leftharpoondown> "CONST transport_const A B x y p"
  "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u"
  "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p"
  "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
  "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f"
  "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f"
*)


end