blob: 703f1aa281618b961dea386a1b0a0fd2ccc41b4e (
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
|
(* Title: HoTT/HoTT_Base.thy
Author: Josh Chen
Date: Jun 2018
Basic setup and definitions of a homotopy type theory object logic.
*)
theory HoTT_Base
imports Pure
begin
section ‹Foundational definitions›
text "A single meta-type ‹Term› suffices to implement the object-logic types and terms."
typedecl 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 used by the simplification method as equational rewrite rules."
named_theorems wellform
named_theorems comp
section ‹Judgments›
text "Formalize the context and typing judgments ‹a : A›.
For judgmental equality we use the existing Pure equality ‹≡› and hence do not need to define a separate judgment for it."
consts
is_of_type :: "[Term, Term] ⇒ prop" ("(1_ : _)" [0, 0] 1000)
section ‹Universes›
text "Strictly-ordered meta-level natural numbers to index the universes."
typedecl Numeral
axiomatization
O :: Numeral ("0") and
S :: "Numeral ⇒ Numeral" ("S_") and
lt :: "[Numeral, Numeral] ⇒ prop" (infix "<-" 999)
where
Numeral_lt_min: "⋀n. 0 <- S n"
and
Numeral_lt_trans: "⋀m n. m <- n ⟹ S m <- S n"
lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans
― ‹Lets ‹standard› automatically solve inequalities.›
text "Universe types:"
axiomatization
U :: "Numeral ⇒ Term" ("U _")
where
Universe_hierarchy: "⋀i j. i <- j ⟹ U(i) : U(j)"
and
Universe_cumulative: "⋀A i j. ⟦A : U(i); i <- j⟧ ⟹ A : U(j)"
section ‹Type families›
text "We define the following abbreviation constraining the output type of a meta lambda expression when given input of certain type."
abbreviation (input) constrained :: "[Term ⇒ Term, Term, Term] ⇒ prop" ("_: _ ⟶ _")
where "f: A ⟶ B ≡ (⋀x. x : A ⟹ f x : B)"
text "The above is used to define type families, which are just constrained meta-lambdas ‹P: A ⟶ B› where ‹A› and ‹B› are elements of some universe type."
type_synonym Typefam = "Term ⇒ Term"
end
|
