Pre-universe implementation commit

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.