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
|
(********
Isabelle/HoTT: Equality
Feb 2019
********)
theory Equal
imports Prod HoTT_Methods
begin
section \<open>Type definitions\<close>
axiomatization
Eq :: "[t, t, t] \<Rightarrow> t" and
refl :: "t \<Rightarrow> t" and
indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
syntax
"_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100)
translations
"a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b"
axiomatization where
Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and
Equal_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and
Equal_elim: "\<lbrakk>
p: x =[A] y;
x: A;
y: A;
\<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f p : C x y p" and
Equal_comp: "\<lbrakk>
a: A;
\<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f (refl a) \<equiv> f a"
lemmas Equal_form [form]
lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
lemmas Equal_comp [comp]
section \<open>Path induction\<close>
text \<open>We set up rudimentary automation of path induction:\<close>
method path_ind for x y p :: t =
(rule Equal_elim[where ?x=x and ?y=y and ?p=p]; (fact | assumption)?)
section \<open>Properties of equality\<close>
subsection \<open>Symmetry (path inverse)\<close>
definition inv :: "[t, t] \<Rightarrow> t"
where "inv A p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) p"
lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A p: y =[A] x"
unfolding inv_def by derive
lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A (refl a) \<equiv> refl a"
unfolding inv_def by derive
declare
inv_type [intro]
inv_comp [comp]
subsection \<open>Transitivity (path composition)\<close>
schematic_goal transitivity:
assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z"
proof (path_ind x y p, quantify 2)
fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" .
qed (routine add: assms)
syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 110)
translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
lemma pathcomp_type:
assumes "A: U i" "x: A" "y: A" "z: A"
shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"
unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms)
corollary pathcomp_trans:
assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z"
shows "p \<bullet> q: x =\<^sub>A z"
by (routine add: assms pathcomp_type)
lemma pathcomp_comp:
assumes "A: U i" and "a: A"
shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
unfolding pathcomp_def by (derive lems: assms)
declare
pathcomp_type [intro]
pathcomp_trans [intro]
pathcomp_comp [comp]
end
|
