diff options
Diffstat (limited to '')
-rw-r--r-- | HoTT_Base.thy | 111 |
1 files changed, 48 insertions, 63 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 916f6aa..2ad0ac5 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,97 +1,82 @@ -(* Title: HoTT/HoTT_Base.thy - Author: Josh Chen +(* +Title: HoTT_Base.thy +Author: Joshua Chen +Date: 2018 -Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. +Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy. *) theory HoTT_Base - imports Pure -begin - +imports Pure -section \<open>Foundational definitions\<close> +begin -text "Meta syntactic type for object-logic types and terms." -typedecl Term +section \<open>Basic setup\<close> +typedecl t \<comment> \<open>Type of object types and terms\<close> +typedecl ord \<comment> \<open>Type of meta-level numerals\<close> -text " - Formalize the typing judgment \<open>a: A\<close>. - For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it. -" +axiomatization + O :: ord and + Suc :: "ord \<Rightarrow> ord" and + lt :: "[ord, ord] \<Rightarrow> prop" (infix "<" 999) and + leq :: "[ord, ord] \<Rightarrow> prop" (infix "\<le>" 999) +where + lt_Suc [intro]: "n < (Suc n)" and + lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and + leq_min [intro]: "O \<le> n" -judgment has_type :: "[Term, Term] \<Rightarrow> prop" ("(3_:/ _)" [0, 0] 1000) +section \<open>Judgment\<close> -section \<open>Universe hierarchy\<close> +judgment hastype :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)") -text "Finite meta-ordinals to index the universes." -typedecl Ord +section \<open>Universes\<close> axiomatization - O :: Ord and - S :: "Ord \<Rightarrow> Ord" ("S _" [0] 1000) and - lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<" 999) and - leq :: "[Ord, Ord] \<Rightarrow> prop" (infix "\<le>" 999) + U :: "ord \<Rightarrow> t" where - lt_min: "\<And>n. O < S n" -and - lt_monotone1: "\<And>n. n < S n" -and - lt_monotone2: "\<And>m n. m < n \<Longrightarrow> S m < S n" -and - leq_min: "\<And>n. O \<le> n" -and - leq_monotone1: "\<And>n. n \<le> S n" -and - leq_monotone2: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n" - -lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2 - \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> - -text "Define the universe types." + U_hierarchy: "i < j \<Longrightarrow> U i: U j" and + U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and + U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j" -axiomatization - U :: "Ord \<Rightarrow> Term" -where - U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U i: U j" -and - U_cumulative: "\<And>A i j. \<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. -text " - The rule \<open>U_cumulative\<close> is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! - To avoid this, it should be instantiated before being applied. -" +@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}. +\<close> section \<open>Type families\<close> -text " - The following abbreviation constrains the output type of a meta lambda expression when given input of certain type. -" - -abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop" ("(1_: _ \<longrightarrow> _)") +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 " - The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types. -" +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 Typefam = "Term \<Rightarrow> Term" +type_synonym tf = "t \<Rightarrow> t" \<comment> \<open>Type of type families\<close> section \<open>Named theorems\<close> -text " - Named theorems to be used by proof methods later (see HoTT_Methods.thy). - - \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting. -" - -named_theorems wellform named_theorems comp +named_theorems form + +text \<open> +Declare named theorems to 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. + +@{attribute form} declares type formation rules. +These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes. +\<close> + +(* Todo: Set up the Simplifier! *) end |