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
|
(********
Isabelle/HoTT: Coproduct, unit, and empty types
Feb 2019
********)
theory More_Types
imports HoTT_Base
begin
section \<open>Coproduct type\<close>
axiomatization
Cprd :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and
inl :: "[t, t, t] \<Rightarrow> t" and
inr :: "[t, t, t] \<Rightarrow> t" and
indCprd :: "[t \<Rightarrow> t, t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
where
Cprd_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and
Cprd_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl A B a: A + B" and
Cprd_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr A B b: A + B" and
Cprd_elim: "\<lbrakk>
u: A + B;
C: A + B \<leadsto> U i;
\<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
\<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d u: C u" and
Cprd_cmp_inl: "\<lbrakk>
a: A;
C: A + B \<leadsto> U i;
\<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
\<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inl A B a) \<equiv> c a" and
Cprd_cmp_inr: "\<lbrakk>
b: B;
C: A + B \<leadsto> U i;
\<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
\<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inr A B b) \<equiv> d b"
lemmas Cprd_form [form]
lemmas Cprd_routine [intro] = Cprd_form Cprd_intro_inl Cprd_intro_inr Cprd_elim
lemmas Cprd_comp [comp] = Cprd_cmp_inl Cprd_cmp_inr
section \<open>Unit type\<close>
axiomatization
Unit :: t and
pt :: t and
indUnit :: "[t \<Rightarrow> t, t, t] \<Rightarrow> t"
where
Unit_form: "Unit: U O" and
Unit_intro: "pt: Unit" and
Unit_elim: "\<lbrakk>x: Unit; c: C pt; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c x: C x" and
Unit_cmp: "\<lbrakk>c: C Unit; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c pt \<equiv> c"
lemmas Unit_form [form]
lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
lemmas Unit_cmp [comp]
section \<open>Empty type\<close>
axiomatization
Null :: t and
indNull :: "[t \<Rightarrow> t, t] \<Rightarrow> t"
where
Null_form: "Null: U O" and
Null_elim: "\<lbrakk>z: Null; C: Null \<leadsto> U i\<rbrakk> \<Longrightarrow> indNull C z: C z"
lemmas Null_form [form]
lemmas Null_routine [intro] = Null_form Null_elim
end
|
