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
|
(********
Isabelle/HoTT: Univalence
Feb 2019
********)
theory Univalence
imports Equivalence
begin
schematic_goal type_eq_imp_equiv:
assumes [intro]: "A: U i" "B: U i"
shows "?prf: A =[U i] B \<rightarrow> A \<cong> B"
unfolding equivalence_def
apply (rule Prod_routine, rule Sum_routine)
prefer 3 apply (derive lems: transport_biinv)
done
(* Copy-paste the derived proof term as the definition of idtoeqv for now;
should really have some automatic export of proof terms, though.
*)
definition idtoeqv :: "[ord, t, t] \<Rightarrow> t" ("(2idtoeqv[_, _, _])") where "
idtoeqv[i, A, B] \<equiv>
\<lambda>p: A =[U i] B.
< transport[U i, Id, A, B]`p, <
< transport[U i, Id, B, A]`(inv[U i, A, B]`p),
happly[x: A. A]
((transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p)
(id A)
(indEq
(\<lambda>A B p.
(transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p
=[A \<rightarrow> A] id A)
(\<lambda>x. refl (id x)) A B p)
>,
< transport[U i, Id, B, A]`(inv[U i, A, B]`p),
happly[x: B. B]
((transport[U i, Id, A, B]`p) o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p)))
(id B)
(indEq
(\<lambda>A B p.
transport[U i, Id, A, B]`p o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p))
=[B \<rightarrow> B] id B)
(\<lambda>x. refl (id x)) A B p)
>
>
>
"
corollary idtoeqv_type:
assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B"
shows "idtoeqv[i, A, B]: A =[U i] B \<rightarrow> A \<cong> B"
unfolding idtoeqv_def by (routine add: type_eq_imp_equiv)
declare idtoeqv_type [intro]
text \<open>For now, we use bi-invertibility as our definition of equivalence.\<close>
axiomatization univalance :: "[ord, t, t] \<Rightarrow> t"
where univalence: "univalence i A B: biinv[A, B] idtoeqv[i, A, B]"
end
|
