1. Remove all type inference functionality (feature development moving to another branch).

2. Eq.thy complete.

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>