blob: cfced79197d828406921f499c81b5d1d82fded43 (
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
|
(* Title: HoTT/HoTT_Base.thy
Author: Josh Chen
Date: Jun 2018
Basic setup and definitions of a homotopy type theory object logic without universes.
*)
theory HoTT_Base
imports Pure
begin
section ‹Setup›
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 used when simplifying function application."
named_theorems wellform
named_theorems comp
section ‹Metalogical definitions›
text "A single meta-type ‹Term› suffices to implement the object-logic types and terms.
We do not implement universes, and simply use ‹a : U› as a convenient shorthand to mean ``‹a› is a type''."
typedecl Term
section ‹Judgments›
text "We formalize the judgments ‹a : A› and ‹A : U› separately, in contrast to the HoTT book where the latter is considered an instance of the former.
For judgmental equality we use the existing Pure equality ‹≡› and hence do not need to define a separate judgment for it."
consts
is_a_type :: "Term ⇒ prop" ("(1_ : U)" [0] 1000)
is_of_type :: "[Term, Term] ⇒ prop" ("(1_ : _)" [0, 0] 1000)
text "The following fact is used to make explicit the assumption of well-formed contexts."
axiomatization where
inhabited_implies_type [intro, elim, wellform]: "⋀a A. a : A ⟹ A : U"
section ‹Type families›
text "A (one-variable) type family is a meta lambda term ‹P :: Term ⇒ Term› that further satisfies the following property."
type_synonym Typefam = "Term ⇒ Term"
abbreviation (input) is_type_family :: "[Typefam, Term] ⇒ prop" ("(3_:/ _ → U)")
where "P: A → U ≡ (⋀x. x : A ⟹ P x : U)"
― ‹There is an obvious generalization to multivariate type families, but implementing such an abbreviation would probably involve writing ML code, and is for the moment not really crucial.›
end
|
