diff options
| author | Josh Chen | 2019-01-30 15:43:47 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-01-30 15:43:47 +0100 |
| commit | a245a3e2194b4d5a6e7fbac8fa10598e96307e57 (patch) | |
| tree | 4c2b5a5dfd940f00f38436e1f00e084f5358d360 /HoTT_Base.thy | |
| parent | 55c148073df8de5f0cf4c45db23d2e3da7f4f093 (diff) | |
Begin refactor
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 19 |
1 files 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> |