aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
authorJosh Chen2020-04-03 01:13:29 +0200
committerJosh Chen2020-04-03 01:13:34 +0200
commit97f3c05e0511a1ed9a95babc800a8e3f3b6a2ea8 (patch)
treeb435de3037203e615d606d9c85fea6927ff6919d /hott/Nat.thy
parent2781c68f0fdb435827097efc497c2172d6050e50 (diff)
1. Base theory. 2. Fix Nat axioms, addition.
Diffstat (limited to 'hott/Nat.thy')
-rw-r--r--hott/Nat.thy19
1 files changed, 10 insertions, 9 deletions
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