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
|
(*
Title: Univalence.thy
Author: Joshua Chen
Date: 2018
Definitions of homotopy, equivalence and the univalence axiom.
*)
theory Univalence
imports HoTT_Methods Equality Prod Sum
begin
section ‹Homotopy and equivalence›
definition homotopic :: "[t, tf, t, t] ⇒ t" where "homotopic A B f g ≡ ∏x:A. (f`x) =[B x] (g`x)"
syntax "_homotopic" :: "[t, idt, t, t, t] ⇒ t" ("(1_ ~[_:_. _]/ _)" [101, 0, 0, 0, 101] 100)
translations "f ~[x:A. B] g" ⇌ "CONST homotopic A (λx. B) f g"
declare homotopic_def [comp]
definition isequiv :: "[t, t, t] ⇒ t" ("(3isequiv[_, _]/ _)") where
"isequiv[A, B] f ≡ (∑g: B → A. g ∘ f ~[x:A. A] id) × (∑g: B → A. f ∘ g ~[x:B. B] id)"
text ‹
The meanings of the syntax defined above are:
▪ @{term "f ~[x:A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "∏x:A. B x"}.
▪ @{term "isequiv[A, B] f"} expresses that the non-dependent function @{term f} of type @{term "A → B"} is an equivalence.
›
definition equivalence :: "[t, t] ⇒ t" (infix "≃" 100)
where "A ≃ B ≡ ∑f: A → B. isequiv[A, B] f"
lemma id_isequiv:
assumes "A: U i" "id: A → A"
shows "<<id, ❙λx. refl x>, <id, ❙λx. refl x>>: isequiv[A, A] id"
unfolding isequiv_def proof (routine add: assms)
show "⋀g. g: A → A ⟹ id ∘ g ~[x:A. A] id: U i" by (derive lems: assms)
show "<id, ❙λx. refl x>: ∑g:A → A. (g ∘ id) ~[x:A. A] id" by (derive lems: assms)
show "<id, ❙λx. refl x>: ∑g:A → A. (id ∘ g) ~[x:A. A] id" by (derive lems: assms)
qed
lemma equivalence_symm:
assumes "A: U i" and "id: A → A"
shows "<id, <<id, ❙λx. refl x>, <id, ❙λx. refl x>>>: A ≃ A"
unfolding equivalence_def proof
show "⋀f. f: A → A ⟹ isequiv[A, A] f: U i" by (derive lems: assms isequiv_def)
show "<<id, ❙λx. refl x>, <id, ❙λx. refl x>>: isequiv[A, A] id" using assms by (rule id_isequiv)
qed fact
section ‹idtoeqv›
definition idtoeqv :: t where "idtoeqv ≡ ❙λp. <transport p, ind⇩= (λ_. <<id, ❙λx. refl x>, <id, ❙λx. refl x>>) p>"
text ‹We prove that equal types are equivalent. The proof involves universe types.›
theorem
assumes "A: U i" and "B: U i"
shows "idtoeqv: (A =[U i] B) → A ≃ B"
unfolding idtoeqv_def equivalence_def proof (routine add: assms)
show *: "⋀f. f: A → B ⟹ isequiv[A, B] f: U i"
unfolding isequiv_def by (derive lems: assms)
show "⋀p. p: A =[U i] B ⟹ transport p: A → B"
by (derive lems: assms transport_type[where ?i="Suc i"])
― ‹Instantiate @{thm transport_type} with a suitable universe level here...›
show "⋀p. p: A =[U i] B ⟹ ind⇩= (λ_. <<id, ❙λx. refl x>, <id, ❙λx. refl x>>) p: isequiv[A, B] (transport p)"
proof (elim Equal_elim)
show "⋀T. T: U i ⟹ <<id, ❙λx. refl x>, <id, ❙λx. refl x>>: isequiv[T, T] (transport (refl T))"
by (derive lems: transport_comp[where ?i="Suc i" and ?A="U i"] id_isequiv)
― ‹...and also here.›
show "⋀A B p. ⟦A: U i; B: U i; p: A =[U i] B⟧ ⟹ isequiv[A, B] (transport p): U i"
unfolding isequiv_def by (derive lems: assms transport_type)
qed fact+
qed (derive lems: assms)
section ‹The univalence axiom›
axiomatization univalence :: "[t, t] ⇒ t" where UA: "univalence A B: isequiv[A, B] idtoeqv"
end
|
