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
106
107
108
109
|
theory HoTT
imports Pure
begin
section ‹Setup›
text ‹
For ML files, routines and setup.
›
section ‹Basic definitions›
text ‹
A single meta-level type ‹Term› suffices to implement the object-level types and terms.
For now we do not implement universes, but simply follow the informal notation in the HoTT book.
› (* Actually unsure if a single meta-type suffices... *)
typedecl Term
subsection ‹Judgements›
consts
is_a_type :: "Term ⇒ prop" ("(_ : U)" [0] 1000)
is_of_type :: "Term ⇒ Term ⇒ prop" ("(3_ :/ _)" [0, 0] 1000)
subsection ‹Basic axioms›
subsubsection ‹Definitional equality›
text‹
We take the meta-equality ≡, defined by the Pure framework for any of its terms,
and use it additionally for definitional/judgmental equality of types and terms in our theory.
Note that the Pure framework already provides axioms and results for the various properties of ≡,
which we make use of and extend where necessary.
›
subsubsection ‹Type-related properties›
axiomatization where
term_substitution: "⋀(A::Term) (x::Term) y::Term. x ≡ y ⟹ A(x) ≡ A(y)" and
equal_types: "⋀(A::Term) (B::Term) x::Term. ⟦A ≡ B; x : A⟧ ⟹ x : B" and
inhabited_implies_type: "⋀(x::Term) A::Term. x : A ⟹ A : U"
subsection ‹Basic types›
subsubsection ‹Nondependent function type›
(*
Write this for now to test stuff, later I should make
this an instance of the dependent function.
Same for the nondependent product below.
Note that the syntax ❙λ (bold lambda) clashes with the proof term syntax!
(See §2.5.2, The Isabelle/Isar Implementation.)
*)
axiomatization
Function :: "Term ⇒ Term ⇒ Term" (infixr "→" 10) and
lambda :: "Term ⇒ Term ⇒ Term ⇒ Term" ("(3❙λ_:_./ _)" [1000, 0, 0] 10) and
appl :: "Term ⇒ Term ⇒ Term" ("(3_`/_)" [10, 10] 10)
where
Function_form: "⋀(A::Term) B::Term. ⟦A : U; B : U⟧ ⟹ A→B : U" and
Function_intro: "⋀(A::Term) (B::Term) b::Term. (⋀x. x : A ⟹ b(x) : B) ⟹ ❙λx:A. b(x) : A→B" and
Function_elim: "⋀A B f a. ⟦f : A→B; a : A⟧ ⟹ f`a : B"
(* beta and eta reductions should go here *)
subsubsection ‹Nondependent product type›
axiomatization
Product :: "Term ⇒ Term ⇒ Term" ("(_×/ _)") and
pair :: "Term ⇒ Term ⇒ Term" ("(_,/ _)") and
rec_Product :: "Term ⇒ Term ⇒ Term ⇒ Term ⇒ Term" ("(rec'_Product'(_,_,_,_'))")
where
Product_form: "⋀A B. ⟦A : U; B : U⟧ ⟹ A×B : U" and
Product_intro: "⋀A B a b. ⟦a : A; b : B⟧ ⟹ (a,b) : A×B" and
Product_elim: "⋀A B C g. ⟦A : U; B : U; C : U; g : A→B→C⟧ ⟹ rec_Product(A,B,C,g) : (A×B)→C" and
Product_comp: "⋀A B C g a b. ⟦C : U; g : A→B→C; a : A; b : B⟧ ⟹ rec_Product(A,B,C,g)`(a,b) ≡ (g`a)`b"
― ‹Projection onto first component›
definition proj1 :: "Term ⇒ Term ⇒ Term" ("(proj1⟨_,_⟩)") where
"proj1⟨A,B⟩ ≡ rec_Product(A, B, A, ❙λx. ❙λy. x)"
subsubsection ‹Empty type›
axiomatization
Null :: Term and
ind_Null :: "Term ⇒ Term ⇒ Term" ("(ind'_Null'(_,/ _'))")
where
Null_form: "Null : U" and
Null_elim: "⋀C x a. ⟦x : Null ⟹ C(x) : U; a : Null⟧ ⟹ ind_Null(C(x), a) : C(a)"
subsubsection ‹Natural numbers›
axiomatization
Nat :: Term and
zero :: Term ("0") and
succ :: "Term ⇒ Term" and (* how to enforce ‹succ : Nat→Nat›? *)
ind_Nat :: "Term ⇒ Term ⇒ Term ⇒ Term ⇒ Term"
where
Nat_form: "Nat : U" and
Nat_intro1: "0 : Nat" and
Nat_intro2: "⋀n. n : Nat ⟹ succ n : Nat"
(* computation rules *)
subsubsection ‹Equality type›
axiomatization
Equal :: "Term ⇒ Term ⇒ Term ⇒ Term" ("(_ =_ _)") and
refl :: "Term ⇒ Term" ("(refl'(_'))")
where
Equal_form: "⋀A a b. ⟦a : A; b : A⟧ ⟹ a =A b : U" and
Equal_intro: "⋀A x. x : A ⟹ refl x : x =A x"
end
|
