aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-07-11 11:08:12 +0200
committerJosh Chen2018-07-11 11:08:12 +0200
commita85feff048010fa945c0e498e45aa5626f54f352 (patch)
treea734741de7bd8ff7368da98bf89bd7793bd85ef9
parent6389f18fd17e4333aba3fcdcc9ed2810d4cb1da5 (diff)
Alternative implementation of universes using meta-level numerals.
-rw-r--r--HoTT_Base.thy75
1 files changed, 43 insertions, 32 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index d119c1f..610e5d8 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -2,7 +2,7 @@
Author: Josh Chen
Date: Jun 2018
-Basic setup and definitions of a homotopy type theory object logic without universes.
+Basic setup and definitions of a homotopy type theory object logic.
*)
theory HoTT_Base
@@ -10,6 +10,13 @@ theory HoTT_Base
begin
+section \<open>Foundational definitions\<close>
+
+text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms."
+
+typedecl Term
+
+
section \<open>Named theorems\<close>
text "Named theorems to be used by proof methods later (see HoTT_Methods.thy).
@@ -21,49 +28,53 @@ named_theorems wellform
named_theorems comp
-section \<open>Foundational definitions\<close>
+section \<open>Judgments\<close>
-text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
-We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''."
+text "Formalize the basic judgments.
-typedecl Term
+For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
+The judgment \<open>is_a_type A\<close> expresses the statement ``A is an inhabitant of some universe type'', i.e. ``A is a type''."
-section \<open>Universes\<close>
+consts
+ is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 1000] 1000)
+ is_a_type :: "Term \<Rightarrow> prop" ("(1_ : U)" [0] 1000)
-ML \<open>
-(* Produces universe terms and judgments on-the-fly *)
-fun Ui_type_oracle (x: int) =
- let
- val f = Sign.declare_const @{context} ((Binding.name ("U" ^ Int.toString x), @{typ Term}), NoSyn);
- val (trm, thy) = f @{theory};
- in
- Theory.setup (fn thy => #2 (f thy));
- Thm.cterm_of (Proof_Context.init_global thy) (trm)
- end
-\<close>
-
-(*
-Sign.add_consts: (binding * typ * mixfix) list -> theory -> theory
-Thm.cterm_of: Proof.context -> term -> cterm
-Thm.add_oracle: binding * (’a -> cterm) -> theory -> (string * (’a -> thm)) * theory
-*)
+text "The following fact is used to make explicit the assumption of well-formed contexts."
-section \<open>Judgments\<close>
+axiomatization where
+ inhabited_implies_type [intro, elim, wellform]: "\<And>a A. a : A \<Longrightarrow> A : U"
-text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> 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 \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it."
+section \<open>Universes\<close>
-consts
- is_a_type :: "Term \<Rightarrow> prop" ("(1_ : U)" [0] 1000)
- is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000)
+text "Strictly-ordered meta-level natural numbers to index the universes."
-text "The following fact is used to make explicit the assumption of well-formed contexts."
+typedecl Numeral
-axiomatization where
- inhabited_implies_type [intro, elim, wellform]: "\<And>a A. a : A \<Longrightarrow> A : U"
+axiomatization
+ O :: Numeral ("0") and
+ S :: "Numeral \<Rightarrow> Numeral" ("S_") and
+ lt :: "[Numeral, Numeral] \<Rightarrow> prop" (infix "<-" 999)
+where
+ Numeral_lt_min: "\<And>n. 0 <- S n"
+and
+ Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n"
+
+\<comment> \<open>This lets \<open>standard\<close> prove ordering statements on Numerals.\<close>
+lemmas Numeral_lt_rules [intro] = Numeral_lt_min Numeral_lt_trans
+
+text "Universe types:"
+
+axiomatization
+ U :: "Numeral \<Rightarrow> Term" ("U_")
+where
+ Universe_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)"
+and
+ Universe_cumulative: "\<And>a i j. \<lbrakk>a : U(i); i <- j\<rbrakk> \<Longrightarrow> a : U(j)"
+
+lemmas Universe_rules [intro] = Universe_hierarchy Universe_cumulative
section \<open>Type families\<close>