From a245a3e2194b4d5a6e7fbac8fa10598e96307e57 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 30 Jan 2019 15:43:47 +0100
Subject: Begin refactor

---
 HoTT_Base.thy | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 9e8fee7..93ef70e 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,9 +1,7 @@
 (*
-Title:  HoTT_Base.thy
-Author: Joshua Chen
-Date:   2018
+Homotopy Type Theory
 
-Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy.
+Foundational setup and definitions
 *)
 
 theory HoTT_Base
@@ -11,13 +9,12 @@ imports Pure
 
 begin
 
-
 section \<open>Basic setup\<close>
 
 declare[[eta_contract=false]]
 
-typedecl t  \<comment> \<open>Type of object types and terms\<close>
-typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
+typedecl t  \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
+typedecl ord  \<comment> \<open>Type of meta-numerals\<close>
 
 axiomatization
   O   :: ord and
@@ -34,12 +31,10 @@ declare
   leq_min [intro!]
   lt_trans [intro]
 
-
-section \<open>Judgment\<close>
+section \<open>Typing judgment\<close>
 
 judgment hastype :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
-
 section \<open>Universes\<close>
 
 axiomatization
@@ -50,8 +45,8 @@ where
   U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
 
 text \<open>
-Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
-One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
+Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination.
+Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 
 @{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}.
 \<close>
-- 
cgit v1.2.3