diff options
| -rw-r--r-- | HoTT_Base.thy | 33 |
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 |