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

---
 HoTT_Base.thy | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 07fbfc4..efc6182 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,7 +1,9 @@
-(*  Title:  HoTT/HoTT_Base.thy
-    Author: Joshua Chen
+(*
+Title:  HoTT_Base.thy
+Author: Joshua Chen
+Date:   2018
 
-Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy.
+Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy.
 *)
 
 theory HoTT_Base
@@ -49,8 +51,8 @@ Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blind
 One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
 \<close>
 
-method cumulativity = (elim U_cumulative, proveSuc)  \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>.\<close>
-method hierarchy = (rule U_hierarchy, proveSuc)  \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...)).\<close>\<close>
+method cumulativity = (elim U_cumulative, proveSuc)  \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>\<close>
+method hierarchy = (rule U_hierarchy, proveSuc)  \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...))\<close>\<close>
 
 
 section \<open>Type families\<close>
@@ -59,22 +61,23 @@ abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> pro
   where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)"
 
 text \<open>
-The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"} where @{term "A::t"} and @{term "B::t"} are small types.
+The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"}, where @{term "A::t"} and @{term "B::t"} are small types.
 \<close>
 
-type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families.\<close>
+type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<close>
 
 
 section \<open>Named theorems\<close>
 
+named_theorems comp
+
 text \<open>
 Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
-\<open>wellform\<close> declares necessary well-formedness conditions for type and inhabitation judgments.
-\<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+@{attribute comp} declares computation rules.
+These are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
 \<close>
 
-named_theorems wellform
-named_theorems comp
+(* Todo: Set up the simplifier! *)
 
 
 end
-- 
cgit v1.2.3