Reorganized HoTT_Base, updated theories

1 files changed, 18 insertions, 18 deletions

diff --git a/Nat.thy b/Nat.thy
index 45c3a2e..a82e7cb 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -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:"