diff options
author | Josh Chen | 2018-07-09 11:17:50 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-09 11:17:50 +0200 |
commit | 6389f18fd17e4333aba3fcdcc9ed2810d4cb1da5 (patch) | |
tree | 33665cf1631895d723a031536dfcf8cc15ecf932 /HoTT_Base.thy | |
parent | decb363a30a30c1875bf4b93bc544c28edf3149e (diff) |
Pre-universe implementation commit
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 60e5167..d119c1f 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -10,7 +10,7 @@ theory HoTT_Base begin -section \<open>Setup\<close> +section \<open>Named theorems\<close> text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). @@ -21,7 +21,7 @@ named_theorems wellform named_theorems comp -section \<open>Metalogical definitions\<close> +section \<open>Foundational definitions\<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''." @@ -29,6 +29,27 @@ We do not implement universes, and simply use \<open>a : U\<close> as a convenie typedecl Term +section \<open>Universes\<close> + +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 +*) + + section \<open>Judgments\<close> 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. |