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
|
(* Title: HoTT/EqualProps.thy
Author: Josh Chen
Date: Jun 2018
Properties of equality.
*)
theory EqualProps
imports
HoTT_Methods
Equal
Prod
begin
section ‹Symmetry / Path inverse›
definition inv :: "[Term, Term] ⇒ (Term ⇒ Term)" ("(1inv[_,/ _])")
where "inv[x,y] ≡ λp. ind⇩= (λx. refl(x)) x y p"
lemma inv_type:
assumes "A : U(i)" and "x : A" and "y : A" and "p: x =⇩A y" shows "inv[x,y](p): y =⇩A x"
unfolding inv_def
proof
show "⋀x y. ⟦x: A; y: A⟧ ⟹ y =⇩A x: U(i)" using assms(1) ..
show "⋀x. x: A ⟹ refl x: x =⇩A x" ..
qed (fact assms)+
lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) ≡ refl(a)"
unfolding inv_def
proof
show "⋀x. x: A ⟹ refl x: x =⇩A x" ..
show "⋀x. x: A ⟹ x =⇩A x: U(i)" using assms(1) ..
qed (fact assms)
section ‹Transitivity / Path composition›
text "``Raw'' composition function, of type ‹∏x,y:A. x =⇩A y → (∏z:A. y =⇩A z → x =⇩A z)›."
definition rcompose :: "Term ⇒ Term" ("(1rcompose[_])")
where "rcompose[A] ≡ ❙λx:A. ❙λy:A. ❙λp:(x =⇩A y). indEqual[A]
(λx y _. ∏z:A. y =⇩A z → x =⇩A z)
(λx. ❙λz:A. ❙λp:(x =⇩A z). indEqual[A](λx z _. x =⇩A z) (λx. refl(x)) x z p)
x y p"
definition compose :: "[Term, Term, Term] ⇒ [Term, Term] ⇒ Term" ("(1compose[ _,/ _,/ _])")
where "compose[x,y,z] ≡ λp."
lemma compose_type:
assumes "A : U(i)" and "x : A" and "y : A" and "z : A"
shows "compose[A,x,y,z] : x =⇩A y → y =⇩A z → x =⇩A z"
unfolding rcompose_def
by (derive lems: assms)
lemma compose_comp:
assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) ≡ refl(a)"
unfolding rcompose_def
by (simplify lems: assms)
lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp
lemmas EqualProps_comps [comp] = inv_comp compose_comp
end
|
