From 76ac8ed82317f3f62f26ecc88f412c61004bcffa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 13:13:55 +0200
Subject: Reorganizing theories

---
 Nat.thy | 60 +++++++++++++++++++++++++++---------------------------------
 1 file changed, 27 insertions(+), 33 deletions(-)

(limited to 'Nat.thy')

diff --git a/Nat.thy b/Nat.thy
index a82e7cb..46b1af5 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -1,54 +1,48 @@
-(*  Title:  HoTT/Nat.thy
-    Author: Josh Chen
+(*
+Title:  Nat.thy
+Author: Joshua Chen
+Date:   2018
 
 Natural numbers
 *)
 
 theory Nat
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and type rules\<close>
 
 axiomatization
-  Nat :: t   ("\<nat>") and
-  zero :: t  ("0") and
-  succ :: "t \<Rightarrow> t" and
+  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"
-and
-  Nat_intro_0: "0: \<nat>"
-and
-  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>"
-and
+  Nat_form: "\<nat>: U O" and
+
+  Nat_intro_0: "0: \<nat>" and
+
+  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;
-    n: \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n"
-and
+    n: \<nat>;
+    C: \<nat> \<longrightarrow> U i;
+    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a n: C n" and
+
   Nat_comp_0: "\<lbrakk>
+    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
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a"
-and
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) 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;
-    n: \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
-
-
-text "Rule attribute declarations:"
+    n: \<nat>;
+    C: \<nat> \<longrightarrow> U i;
+    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
-lemmas Nat_intro = Nat_intro_0 Nat_intro_succ
-lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ
-lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim
+lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
+lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
 
 
 end
-- 
cgit v1.2.3


From 6857e783fa5cb91f058be322a18fb9ea583f2aad Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 11:38:54 +0200
Subject: Overhaul of the theory presentations. New methods in HoTT_Methods.thy
 for handling universes. Commit for release 0.1.0!

---
 Nat.thy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Nat.thy')

diff --git a/Nat.thy b/Nat.thy
index 46b1af5..8a55852 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -41,6 +41,7 @@ where
     C: \<nat> \<longrightarrow> U i;
     \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
+lemmas Nat_form [form]
 lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
 lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
 
-- 
cgit v1.2.3