aboutsummaryrefslogtreecommitdiff
path: root/hott/Equivalence.thy
blob: c888714c4812a0f9aef386d72e53e6324d1a11f8 (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
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
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 [type]:
  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 apply_homotopy:
  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"
    "H: f ~ g"
    "x: A"
  shows "H x: f x = g x"
  using \<open>H:_\<close> unfolding homotopy_def
  by typechk

method htpy for H::o = rule apply_homotopy[where ?H=H]

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

Lemma (def) hsym:
  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"
    "H: f ~ g"
  shows "g ~ f"
  unfolding homotopy_def
  proof intro
    fix x assuming "x: A" then have "f x = g x"
      by (htpy H)
    thus "g x = f x"
      by (rule pathinv) fact
  qed

Lemma (def) htrans:
  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"
    "h: \<Prod>x: A. B x"
    "H1: f ~ g"
    "H2: g ~ h"
  shows "f ~ h"
  unfolding homotopy_def
  proof intro
    fix x assuming "x: A"
    have *: "f x = g x" "g x = h x"
      by (htpy H1, htpy H2)
    show "f x = h x"
      by (rule pathcomp; (rule *)?) typechk
  qed

section \<open>Rewriting homotopies\<close>

calc "f ~ g" rhs g

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

Lemma id_funcomp_htpy:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "homotopy_refl A f: (id B) \<circ> f ~ f"
  by compute

Lemma funcomp_id_htpy:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "homotopy_refl A f: f \<circ> (id A) ~ f"
  by compute

Lemma funcomp_left_htpy:
  assumes
    "A: U i" "B: U i"
    "\<And>x. x: B \<Longrightarrow> C x: U i"
    "f: A \<rightarrow> B"
    "g: \<Prod>x: B. C x"
    "g': \<Prod>x: B. C x"
    "H: g ~ g'"
  shows "(g \<circ> f) ~ (g' \<circ> f)"
  unfolding homotopy_def
  apply (intro, compute)
  apply (htpy H)
  done

Lemma funcomp_right_htpy:
  assumes
    "A: U i" "B: U i" "C: U i"
    "f: A \<rightarrow> B"
    "f': A \<rightarrow> B"
    "g: B \<rightarrow> C"
    "H: f ~ f'"
  shows "(g \<circ> f) ~ (g \<circ> f')"
  unfolding homotopy_def
  proof (intro, compute)
    fix x assuming "x: A"
    have *: "f x = f' x"
      by (htpy H)
    show "g (f x) = g (f' x)"
      by (rewr eq: *) refl
  qed

method lhtpy = rule funcomp_left_htpy[rotated 6]
method rhtpy = rule funcomp_right_htpy[rotated 6]

Lemma (def) commute_homotopy:
  assumes
    "A: U i" "B: U i"
    "x: A" "y: A"
    "p: x = y"
    "f: A \<rightarrow> B" "g: A \<rightarrow> B"
    "H: f ~ g"
  shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
  using \<open>H:_\<close>
  unfolding homotopy_def
  apply (eq p, compute)
  apply (rewr eq: pathcomp_refl, rewr eq: refl_pathcomp)
  by refl

Corollary (def) commute_homotopy':
  assumes
    "A: U i"
    "x: A"
    "f: A \<rightarrow> A"
    "H: f ~ (id A)"
  shows "H (f x) = f [H x]"
  proof -
   (*FUTURE: Because we don't have very good normalization integrated into
      things yet, we need to manually unfold the type of H.*)
    from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
      by (compute add: homotopy_def)

    have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
      by (rule left_whisker, rewr eq: ap_id, refl)
    also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
      by (rule commute_homotopy)
    finally have "?" by infer

    thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+)
  qed


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

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

definition "is_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 is_qinv_type [type]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "is_qinv A B f: U i"
  unfolding is_qinv_def
  by typechk

definition is_qinv_i ("is'_qinv")
  where [implicit]: "is_qinv f \<equiv> Equivalence.is_qinv {} {} f"

no_translations "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f"

Lemma (def) id_is_qinv:
  assumes "A: U i"
  shows "is_qinv (id A)"
  unfolding is_qinv_def
  proof intro
    show "id A: A \<rightarrow> A" by typechk
  qed (compute, intro; refl)

Lemma is_qinvI:
  assumes
    "A: U i" "B: U i" "f: A \<rightarrow> B"
    "g: B \<rightarrow> A"
    "H1: g \<circ> f ~ id A"
    "H2: f \<circ> g ~ id B"
  shows "is_qinv f"
  unfolding is_qinv_def
  proof intro
    show "g: B \<rightarrow> A" by fact
    show "g \<circ> f ~ id A \<times> f \<circ> g ~ id B" by (intro; fact)
  qed

Lemma is_qinv_components [type]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f"
  shows
    qinv_of_is_qinv: "fst pf: B \<rightarrow> A" and
    ret_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and
    sec_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B"
  using assms unfolding is_qinv_def
  by typechk+

Lemma (def) qinv_is_qinv:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f"
  shows "is_qinv (fst pf)"
  using \<open>pf:_\<close>[unfolded is_qinv_def] \<comment> \<open>Should be unfolded by the typechecker\<close>
  apply (rule is_qinvI)
  \<^item> by (fact \<open>f:_\<close>)
  \<^item> by (rule sec_of_is_qinv)
  \<^item> by (rule ret_of_is_qinv)
  done

Lemma (def) funcomp_is_qinv:
  assumes
    "A: U i" "B: U i" "C: U i"
    "f: A \<rightarrow> B" "g: B \<rightarrow> C"
  shows "is_qinv f \<rightarrow> is_qinv g \<rightarrow> is_qinv (g \<circ> f)"
  apply intros
  unfolding is_qinv_def apply elims
  focus vars _ _ finv _ ginv
    apply intro
    \<^item> by (rule funcompI[where ?f=ginv and ?g=finv])
    \<^item> proof intro
        show "(finv \<circ> ginv) \<circ> g \<circ> f ~ id A"
        proof -
          have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by compute refl
          also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact
          also have ".. ~ id A" by compute fact
          finally show "?" by infer
        qed

        show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C"
        proof -
          have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by compute refl
          also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact
          also have ".. ~ id C" by compute fact
          finally show "?" by infer
        qed
      qed
    done
  done

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

definition "is_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 is_biinv_type [type]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "is_biinv A B f: U i"
  unfolding is_biinv_def by typechk

definition is_biinv_i ("is'_biinv")
  where [implicit]: "is_biinv f \<equiv> Equivalence.is_biinv {} {} f"

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

Lemma is_biinvI:
  assumes
    "A: U i" "B: U i" "f: A \<rightarrow> B"
    "g: B \<rightarrow> A" "h: B \<rightarrow> A"
    "H1: g \<circ> f ~ id A" "H2: f \<circ> h ~ id B"
  shows "is_biinv f"
  unfolding is_biinv_def
  proof intro
    show "<g, H1>: \<Sum>g: B \<rightarrow> A. g \<circ> f ~ id A" by typechk
    show "<h, H2>: \<Sum>g: B \<rightarrow> A. f \<circ> g ~ id B" by typechk
  qed

Lemma is_biinv_components [type]:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_biinv f"
  shows
    section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
    retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
    ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
    sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B"
  using assms unfolding is_biinv_def
  by typechk+

Lemma (def) is_biinv_if_is_qinv:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "is_qinv f \<rightarrow> is_biinv f"
  apply intros
  unfolding is_qinv_def is_biinv_def
  by (rule distribute_Sig)

Lemma (def) is_qinv_if_is_biinv:
  assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
  shows "is_biinv f \<rightarrow> is_qinv f"
  apply intro
  unfolding is_biinv_def apply elims
  focus vars _ _ _ g H1 h H2
    apply (rule is_qinvI)
      \<^item> by (fact \<open>g: _\<close>)
      \<^item> by (fact \<open>H1: _\<close>)
      \<^item> proof -
          have "g ~ g \<circ> (id B)" by compute refl
          also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric])
          also have ".. ~ (id A) \<circ> h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact)
          also have ".. ~ h" by compute refl
          finally have "g ~ h" by infer
          then have "f \<circ> g ~ f \<circ> h" by (rhtpy, infer)
          also note \<open>H2:_\<close>
          finally show "f \<circ> g ~ id B" by infer
        qed
    done
  done

Lemma (def) id_is_biinv:
  "A: U i \<Longrightarrow> is_biinv (id A)"
  by (rule is_biinv_if_is_qinv) (rule id_is_qinv)

Lemma (def) funcomp_is_biinv:
  assumes
    "A: U i" "B: U i" "C: U i"
    "f: A \<rightarrow> B" "g: B \<rightarrow> C"
  shows "is_biinv f \<rightarrow> is_biinv g \<rightarrow> is_biinv (g \<circ> f)"
  apply intros
  focus vars pf pg
    by (rule is_biinv_if_is_qinv)
       (rule funcomp_is_qinv; rule is_qinv_if_is_biinv, fact)
  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.is_biinv A B f"

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

Lemma (def) equivalence_refl:
  assumes "A: U i"
  shows "A \<simeq> A"
  unfolding equivalence_def
  proof intro
    show "is_biinv (id A)" by (rule is_biinv_if_is_qinv) (rule id_is_qinv)
  qed typechk

Lemma (def) equivalence_symmetric:
  assumes "A: U i" "B: U i"
  shows "A \<simeq> B \<rightarrow> B \<simeq> A"
  apply intros
  unfolding equivalence_def
  apply elim
  apply (dest (4) is_qinv_if_is_biinv)
  apply intro
    \<^item> by (rule qinv_of_is_qinv) facts
    \<^item> by (rule is_biinv_if_is_qinv) (rule qinv_is_qinv)
  done

Lemma (def) 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: is_biinv (fst AB)"
      "fst BC: B \<rightarrow> C" and 2: "snd BC: is_biinv (fst BC)"
      unfolding equivalence_def by typechk+
    then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk
    moreover have "is_biinv (fst BC \<circ> fst AB)"
      using * unfolding equivalence_def by (rule funcomp_is_biinv 1 2) facts
    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) typechecker normalization is still
  rudimentary, and (2) we don't yet have universe level inference.
\<close>

Lemma (def) equiv_if_equal:
  notes Ui_in_USi [form]
  assumes
    "A: U i" "B: U i" "p: A = B"
  shows "<transp (id (U i)) p, ?isequiv>: A \<simeq> B"
  unfolding equivalence_def
  apply intro defer
    \<^item> apply (eq p)
      \<^enum> vars A B
        apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
        using [[solve_side_conds=1]]
        apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
        using Ui_in_USi by (rule transport, rule lift_universe_codomain)
      \<^enum> vars A
        apply (comp transport_comp)
          \<circ> by (rule U_lift)
          \<circ> by compute (rule id_is_biinv)
        done
      done

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

Definition idtoeqv: ":= MLTT.fst (A \<rightarrow> B) is_biinv (equiv_if_equal i A B p)"
  where "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
  using equiv_if_equal unfolding equivalence_def
  by typechk

definition idtoeqv_i ("idtoeqv")
  where [implicit]: "idtoeqv p \<equiv> Equivalence.idtoeqv {} {} {} p"


end