diff options
Diffstat (limited to '')
-rw-r--r-- | hott/Nat.thy | 19 |
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 |