From 88df8512841c1f2cb7016d2b604b9250582d4b8d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 16 Apr 2020 15:03:23 +0200
Subject: minor naming

---
 hott/Nat.thy | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/hott/Nat.thy b/hott/Nat.thy
index b88398b..59ec517 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -17,39 +17,43 @@ where
 
   NatE: "\<lbrakk>
     n: Nat;
-    n\<^sub>0: C 0;
+    c\<^sub>0: C 0;
     \<And>n. n: Nat \<Longrightarrow> C n: U i;
     \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k)
-    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) n: C n" and
+    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n: C n" and
 
   Nat_comp_zero: "\<lbrakk>
-    n\<^sub>0: C 0;
+    c\<^sub>0: C 0;
     \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
     \<And>n. n: Nat \<Longrightarrow> C n: U i
-    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) 0 \<equiv> n\<^sub>0" and
+    \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) 0 \<equiv> c\<^sub>0" and
 
   Nat_comp_suc: "\<lbrakk>
     n: Nat;
-    n\<^sub>0: C 0;
+    c\<^sub>0: C 0;
     \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
     \<And>n. n: Nat \<Longrightarrow> C n: U i
     \<rbrakk> \<Longrightarrow>
-      NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) (suc n) \<equiv>
-        f n (NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) n)"
+      NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) (suc n) \<equiv>
+        f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n)"
 
 lemmas
   [intros] = NatF Nat_zero Nat_suc and
   [elims] = NatE and
   [comps] = Nat_comp_zero Nat_comp_suc
 
+text \<open>Non-dependent recursion\<close>
+
+abbreviation "NatRec C \<equiv> NatInd (K C)"
+
 
 section \<open>Basic arithmetic\<close>
 
 definition add (infixl "+" 50) where
-  [comps]: "m + n \<equiv> NatInd (K Nat) n (K suc) m"
+  [comps]: "m + n \<equiv> NatRec Nat n (K suc) m"
 
 definition mul (infixl "*" 55) where
-  [comps]: "m * n \<equiv> NatInd (K Nat) 0 (K $ add n) m"
+  [comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m"
 
 
 end
-- 
cgit v1.2.3