1. Base theory. 2. Fix Nat axioms, addition.

2 files changed, 21 insertions, 11 deletions

diff --git a/hott/Basic_Types.thy b/hott/Base.thy
index 85f22a8..2a4ff9c 100644
--- a/hott/Basic_Types.thy
+++ b/hott/Base.thy
@@ -1,8 +1,17 @@
-theory Basic_Types
-imports Spartan
+theory Base
+imports Spartan.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 f846dbf..269d6bb 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
 theory Nat
-imports Spartan
+imports Base
 
 begin
 
@@ -17,22 +17,22 @@ where
 
   NatE: "\<lbrakk>
     n: Nat;
-    n\<^sub>0: Nat;
+    n\<^sub>0: C 0;
     \<And>n. n: Nat \<Longrightarrow> C n: U i;
     \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (suc n)
     \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>n c. f n c) n: C n" and
 
   Nat_comp_zero: "\<lbrakk>
-    n\<^sub>0: Nat;
-    \<And>n. n: Nat \<Longrightarrow> C n: U i;
-    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (suc n)
+    n\<^sub>0: C 0;
+    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (suc n);
+    \<And>n. n: Nat \<Longrightarrow> C n: U i
     \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>n c. f n c) 0 \<equiv> n\<^sub>0" and
 
   Nat_comp_suc: "\<lbrakk>
     n: Nat;
-    n\<^sub>0: Nat;
-    \<And>n. n: Nat \<Longrightarrow> C n: U i;
-    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (suc n)
+    n\<^sub>0: C 0;
+    \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (suc n);
+    \<And>n. n: Nat \<Longrightarrow> C n: U i
     \<rbrakk> \<Longrightarrow>
       NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>n c. f n c) (suc n) \<equiv>
         f n (NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>n c. f n c) n)"
@@ -45,7 +45,8 @@ lemmas
 
 section \<open>Basic arithmetic\<close>
 
-\<comment> \<open>TODO\<close>
+definition add (infixl "+" 50) where
+  [comps]: "m + n \<equiv> NatInd (K Nat) n (K $ \<lambda>n. suc n) m"
 
 
 end