diff options
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 76 |
1 files changed, 41 insertions, 35 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 8c45d35..cf71813 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,8 +1,8 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen - Date: Jun 2018 + Date: Aug 2018 -Basic setup and definitions of a homotopy type theory object logic. +Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. *) theory HoTT_Base @@ -12,71 +12,77 @@ begin section \<open>Foundational definitions\<close> -text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms." +text "Meta syntactic type for object-logic types and terms." typedecl Term -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 used by the simplification method as equational rewrite rules." - -named_theorems wellform -named_theorems comp - - section \<open>Judgments\<close> -text "Formalize the context and typing judgments \<open>a : A\<close>. - -For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it." +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. +" consts - is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000) + has_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000) -section \<open>Universes\<close> +section \<open>Universe hierarchy\<close> -text "Strictly-ordered meta-level natural numbers to index the universes." +text "Finite meta-ordinals to index the universes." -typedecl Numeral +typedecl Ord axiomatization - O :: Numeral ("0") and - S :: "Numeral \<Rightarrow> Numeral" ("S_") and - lt :: "[Numeral, Numeral] \<Rightarrow> prop" (infix "<-" 999) + O :: Ord and + S :: "Ord \<Rightarrow> Ord" ("S_" [0] 1000) and + lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<-" 999) where - Numeral_lt_min: "\<And>n. 0 <- S n" + Ord_lt_min: "\<And>n. O <- S n" and - Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" + Ord_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" -lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans +lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_trans \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> -text "Universe types:" +text "Define the universe types." axiomatization - U :: "Numeral \<Rightarrow> Term" ("U _") + U :: "Ord \<Rightarrow> Term" where - Universe_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)" + U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)" and - Universe_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)" - \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> + U_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)" + \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> section \<open>Type families\<close> -text "We define the following abbreviation constraining the output type of a meta lambda expression when given input of certain type." +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" ("_: _ \<longrightarrow> _") +abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<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 just constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are elements of some universe type." +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. +" type_synonym Typefam = "Term \<Rightarrow> Term" +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 used by the simplification method as equational rewrite rules. +" + +named_theorems wellform +named_theorems comp + + end
\ No newline at end of file |