diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Base.thy | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1dcf61c..34474d1 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -11,11 +11,20 @@ This file completes the basic logical and functional setup of the HoTT logic. It ********) theory HoTT_Base -imports HoTT_Typing +imports Pure begin +section \<open>Basic setup\<close> + +declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close> + +typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close> + +judgment has_type :: "[t, t] \<Rightarrow> prop" ("(2_ :/ _)") + + section \<open>Universes\<close> typedecl ord \<comment> \<open>Type of meta-numerals\<close> |