blob: 916f6aa24353c9c18b00ebe3d5ab4bbe1e1c8d4c (
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
(* Title: HoTT/HoTT_Base.thy
Author: Josh Chen
Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell.
*)
theory HoTT_Base
imports Pure
begin
section ‹Foundational definitions›
text "Meta syntactic type for object-logic types and terms."
typedecl Term
text "
Formalize the typing judgment ‹a: A›.
For judgmental/definitional equality we use the existing Pure equality ‹≡› and hence do not need to define a separate judgment for it.
"
judgment has_type :: "[Term, Term] ⇒ prop" ("(3_:/ _)" [0, 0] 1000)
section ‹Universe hierarchy›
text "Finite meta-ordinals to index the universes."
typedecl Ord
axiomatization
O :: Ord and
S :: "Ord ⇒ Ord" ("S _" [0] 1000) and
lt :: "[Ord, Ord] ⇒ prop" (infix "<" 999) and
leq :: "[Ord, Ord] ⇒ prop" (infix "≤" 999)
where
lt_min: "⋀n. O < S n"
and
lt_monotone1: "⋀n. n < S n"
and
lt_monotone2: "⋀m n. m < n ⟹ S m < S n"
and
leq_min: "⋀n. O ≤ n"
and
leq_monotone1: "⋀n. n ≤ S n"
and
leq_monotone2: "⋀m n. m ≤ n ⟹ S m ≤ S n"
lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2
― ‹Enables ‹standard› to automatically solve inequalities.›
text "Define the universe types."
axiomatization
U :: "Ord ⇒ Term"
where
U_hierarchy: "⋀i j. i < j ⟹ U i: U j"
and
U_cumulative: "⋀A i j. ⟦A: U i; i ≤ j⟧ ⟹ A: U j"
text "
The rule ‹U_cumulative› is very unsafe: if used as-is it will usually lead to an infinite rewrite loop!
To avoid this, it should be instantiated before being applied.
"
section ‹Type families›
text "
The following abbreviation constrains the output type of a meta lambda expression when given input of certain type.
"
abbreviation (input) constrained :: "[Term ⇒ Term, Term, Term] ⇒ prop" ("(1_: _ ⟶ _)")
where "f: A ⟶ B ≡ (⋀x. x : A ⟹ f x: B)"
text "
The above is used to define type families, which are constrained meta-lambdas ‹P: A ⟶ B› where ‹A› and ‹B› are small types.
"
type_synonym Typefam = "Term ⇒ Term"
section ‹Named theorems›
text "
Named theorems to be used by proof methods later (see HoTT_Methods.thy).
‹wellform› declares necessary wellformedness conditions for type and inhabitation judgments, while ‹comp› declares computation rules, which are usually passed to invocations of the method ‹subst› to perform equational rewriting.
"
named_theorems wellform
named_theorems comp
end
|
