4 files changed, 14 insertions, 12 deletions
diff --git a/hott/HoTT.thy b/hott/HoTT.thy
new file mode 100644
index 0000000..0b3040c
--- /dev/null
+++ b/hott/HoTT.thy
@@ -0,0 +1,10 @@
+theory HoTT
+imports
+  Identity
+  Equivalence
+  More_Types
+  Nat
+
+begin
+
+end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 3a982f6..3fef536 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -30,13 +30,13 @@ axiomatization where
     b: A;
     \<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i;
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
-    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a b p: C a b p" and
+    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a b p: C a b p" and
 
   Id_comp: "\<lbrakk>
     a: A;
     \<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i;
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
-    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a a (refl a) \<equiv> f a"
+    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a a (refl a) \<equiv> f a"
 
 lemmas
   [intros] = IdF IdI and
diff --git a/hott/Base.thy b/hott/More_Types.thy
index 610a373..17789f8 100644
--- a/hott/Base.thy
+++ b/hott/More_Types.thy
@@ -1,17 +1,9 @@
-theory Base
+theory More_Types
 imports Equivalence
 
 begin
 
 
-section \<open>Notation\<close>
-
-syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
-translations "a $ b" \<rightharpoonup> "a (b)"
-
-abbreviation (input) K where "K x \<equiv> \<lambda>_. x"
-
-
 section \<open>Sum type\<close>
 
 axiomatization
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 311f2d9..e129be0 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
 theory Nat
-imports Base
+imports Equivalence
 
 begin