diff options
author | Josh Chen | 2018-09-16 11:03:48 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-16 11:03:48 +0200 |
commit | d4900ced2e071927d81a21a9127034941f258ec3 (patch) | |
tree | c0289b3fd8337a05baa7740ca3f5e84c57f539ca /Nat.thy | |
parent | 515872533295e8464799467303fff923b52a2c01 (diff) | |
parent | f0999d07a0f41284ba84fae725a0186e0ec9ff5f (diff) |
Reorganized HoTT_Base, updated theories
Diffstat (limited to 'Nat.thy')
-rw-r--r-- | Nat.thy | 36 |
1 files changed, 18 insertions, 18 deletions
@@ -12,36 +12,36 @@ begin section \<open>Constants and type rules\<close> axiomatization - Nat :: Term ("\<nat>") and - zero :: Term ("0") and - succ :: "Term \<Rightarrow> Term" and - indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)") + Nat :: t ("\<nat>") and + zero :: t ("0") and + succ :: "t \<Rightarrow> t" and + indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t" ("(1ind\<^sub>\<nat>)") where - Nat_form: "\<nat>: U(O)" + Nat_form: "\<nat>: U O" and Nat_intro_0: "0: \<nat>" and - Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ(n): \<nat>" + Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and Nat_elim: "\<lbrakk> - C: \<nat> \<longrightarrow> U(i); - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); - a: C(0); + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); + a: C 0; n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(n): C(n)" + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" and Nat_comp_0: "\<lbrakk> - C: \<nat> \<longrightarrow> U(i); - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); - a: C(0) - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(0) \<equiv> a" + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n); + a: C 0 + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and Nat_comp_succ: "\<lbrakk> - C: \<nat> \<longrightarrow> U(i); - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); - a: C(0); + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); + a: C 0; n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)" + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" text "Rule attribute declarations:" |