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
110
111
112
113
114
|
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.
We do not implement universes, but simply follow the informal notation in the HoTT book."
typedecl Term
subsection ‹Judgments›
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 various properties of ≡, which we make use of and extend where necessary."
subsubsection ‹Type-related properties›
axiomatization where
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 ‹Dependent product type›
consts
Prod :: "[Term, (Term ⇒ Term)] ⇒ Term"
syntax
"_Prod" :: "[idt, Term, Term] ⇒ Term" ("(3∏_:_./ _)" 10)
translations
"∏x:A. B" ⇌ "CONST Prod A (λx. B)"
(* The above syntax translation binds the x in B *)
axiomatization
lambda :: "(Term ⇒ Term) ⇒ Term" (binder "❙λ" 10) and
appl :: "[Term, Term] ⇒ Term" ("(3_`/_)" [10, 10] 60)
where
Prod_form: "⋀(A::Term) (B::Term ⇒ Term). ⟦A : U; ⋀(x::Term). x : A ⟹ B(x) : U⟧ ⟹ ∏x:A. B(x) : U" and
Prod_intro: "⋀(A::Term) (B::Term ⇒ Term) (b::Term ⇒ Term). ⟦A : U; ⋀(x::Term). x : A ⟹ b(x) : B(x)⟧ ⟹ ❙λx. b(x) : ∏x:A. B(x)" and
Prod_elim: "⋀(A::Term) (B::Term ⇒ Term) (f::Term) (a::Term). ⟦f : ∏x:A. B(x); a : A⟧ ⟹ f`a : B(a)" and
Prod_comp: "⋀(b::Term ⇒ Term) (a::Term). (❙λx. b(x))`a ≡ b(a)" and
Prod_uniq: "⋀(A::Term) (B::Term ⇒ Term) (f::Term). ⟦f : ∏x:A. B(x)⟧ ⟹ ❙λx. (f`x) ≡ f"
text "Observe that the metatype ‹Term ⇒ Term› is used to represent type families, for example ‹Prod› takes a type ‹A› and a type family ‹B› and constructs a dependent function type from them."
text "Note that the syntax ‹❙λ› (bold lambda) used for dependent functions clashes with the proof term syntax (cf. §2.5.2 of the Isabelle/Isar Implementation)."
abbreviation Function :: "[Term, Term] ⇒ Term" (infixr "→" 30)
where "A→B ≡ ∏_:A. B"
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
"⋀A B x y. proj1⟨A,B⟩ ≡ rec_Product(A, B, A, ❙λx:A. ❙λy:B. (λx. 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
|
