blob: e90cd954085c2992260d51e836cc014dd01f2831 (
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
|
(* Title: HoTT/Proj.thy
Author: Josh Chen
Date: Jun 2018
Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type.
*)
theory Proj
imports
HoTT_Methods
Prod
Sum
begin
axiomatization fst :: "Term \<Rightarrow> Term" where fst_def: "fst \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. x)(p)"
axiomatization snd :: "Term \<Rightarrow> Term" where snd_def: "snd \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. y)(p)"
text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
lemma fst_type:
assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
unfolding fst_def
proof
show "A: U(i)" using assms(1) by (rule Sum_wellform)
qed (fact assms | assumption)+
lemma fst_comp:
assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
unfolding fst_def
proof
show "\<And>x. x: A \<Longrightarrow> x: A" .
qed (rule assms)+
lemma snd_type:
assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
unfolding snd_def
proof
show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)"
proof -
have "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> fst(p): A" using assms(1) by (rule fst_type)
with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_wellform)
qed
fix x y
assume asm: "x: A" "y: B(x)"
show "y: B(fst <x,y>)"
proof (subst fst_comp)
show "A: U(i)" using assms(1) by (rule Sum_wellform)
show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_wellform)
qed (rule asm)+
qed (fact assms)
lemma snd_comp:
assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b"
unfolding snd_def
proof
show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
show "a: A" by (fact assms)
show "b: B(a)" by (fact assms)
show *: "B(a): U(i)" using assms(3) by (rule assms(2))
show "B(a): U(i)" by (fact *)
qed
lemmas Proj_comps [intro] = fst_comp snd_comp
end
|
