diff options
author | Josh Chen | 2018-09-17 13:13:55 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-17 13:13:55 +0200 |
commit | 76ac8ed82317f3f62f26ecc88f412c61004bcffa (patch) | |
tree | 02f3f3f5f87027d38520e376c577e7e6621fa6cf /HoTT_Base.thy | |
parent | ea0c0c5427888982adce10ab25cebe445997f08b (diff) |
Reorganizing theories
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 25 |
1 files changed, 14 insertions, 11 deletions
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 |