aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT_Base.thy33
1 files changed, 13 insertions, 20 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 93ef70e..99ab5ce 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,8 +1,15 @@
-(*
-Homotopy Type Theory
+(********
+Isabelle/HoTT: Foundational definitions and notation
+Jan 2019
-Foundational setup and definitions
-*)
+This file is the starting point, and contains the base setup and definitions of the object logic.
+Among other things, it defines:
+
+* Meta-numerals to index the universe hierarchy, and related axioms.
+* The universe hierarchy and its governing rules.
+* Named theorems for later use by proof methods.
+
+********)
theory HoTT_Base
imports Pure
@@ -11,7 +18,7 @@ begin
section \<open>Basic setup\<close>
-declare[[eta_contract=false]]
+declare[[eta_contract=false]] (* I'm not actually sure this does anything... *)
typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
typedecl ord \<comment> \<open>Type of meta-numerals\<close>
@@ -51,26 +58,13 @@ 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>
-
-section \<open>Type families\<close>
-
-abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop" ("(1_:/ _ \<longrightarrow> _)")
- 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.
-\<close>
-
-type_synonym tf = "t \<Rightarrow> t" \<comment> \<open>Type of type families\<close>
-
-
section \<open>Named theorems\<close>
named_theorems comp
named_theorems form
text \<open>
-Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
+The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}.
@{attribute comp} declares computation rules, which 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.
@@ -80,5 +74,4 @@ These are mainly used by the \<open>cumulativity\<close> method, which lifts typ
(* Todo: Set up the Simplifier! *)
-
end