aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--hott/Nat.thy51
1 files changed, 51 insertions, 0 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy
new file mode 100644
index 0000000..f846dbf
--- /dev/null
+++ b/hott/Nat.thy
@@ -0,0 +1,51 @@
+theory Nat
+imports Spartan
+
+begin
+
+axiomatization
+ Nat :: \<open>o\<close> and
+ zero :: \<open>o\<close> ("0") and
+ suc :: \<open>o \<Rightarrow> o\<close> and
+ NatInd :: \<open>(o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+where
+ NatF: "Nat: U i" and
+
+ Nat_zero: "0: Nat" and
+
+ Nat_suc: "n: Nat \<Longrightarrow> suc n: Nat" and
+
+ NatE: "\<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)
+ \<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)
+ \<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)
+ \<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)"
+
+lemmas
+ [intros] = NatF Nat_zero Nat_suc and
+ [elims] = NatE and
+ [comps] = Nat_comp_zero Nat_comp_suc
+
+
+section \<open>Basic arithmetic\<close>
+
+\<comment> \<open>TODO\<close>
+
+
+end