diff options
author | Josh Chen | 2018-06-12 12:30:54 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-12 12:30:54 +0200 |
commit | 91efce41a2319a9fb861ff26d7dc8c49ec726d4c (patch) | |
tree | fd42310d712143e0f3dceff7009309a89b787b92 /HoTT_Base.thy | |
parent | 593faab277de53cbe2cb0c2feca5de307d9334ac (diff) |
Type rules now have \"all\" premises explicitly stated, matching the formulation in the HoTT book.
Diffstat (limited to '')
-rw-r--r-- | HoTT_Base.thy | 44 |
1 files changed, 29 insertions, 15 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9650c4c..9b422c4 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,5 +1,6 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen + Date: Jun 2018 Basic setup and definitions of a homotopy type theory object logic. *) @@ -9,23 +10,43 @@ theory HoTT_Base begin -section \<open>Basic definitions\<close> +section \<open>Setup\<close> -text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms. -We do not implement universes, but simply follow the informal notation in the HoTT book." +text "Set up type checking routines, proof methods etc." + + +section \<open>Metalogical definitions\<close> + +text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms. +Our implementation does not have universes, and we simply use \<open>a : U\<close> as a convenient shorthand meaning ``\<open>a\<close> is a type''." typedecl Term + section \<open>Judgments\<close> consts -is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)" [0] 1000) -is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(3_ :/ _)" [0, 0] 1000) +is_a_type :: "Term \<Rightarrow> prop" ("(1_ :/ U)" [0] 1000) +is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) + + +section \<open>Type families\<close> + +text "A (one-variable) type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property." + +type_synonym Typefam = "Term \<Rightarrow> Term" + +abbreviation is_type_family :: "[Typefam, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)") + where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P x : U)" + +text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial." section \<open>Definitional equality\<close> -text "We use the Pure equality \<open>\<equiv>\<close> for definitional/judgmental equality of types and terms in our theory." +text "The Pure equality \<open>\<equiv>\<close> is used for definitional aka judgmental equality of types and terms." + +\<comment> \<open>Do these ever need to be used? theorem equal_types: assumes "A \<equiv> B" and "A : U" @@ -35,18 +56,11 @@ theorem equal_type_element: assumes "A \<equiv> B" and "x : A" shows "x : B" using assms by simp -lemmas type_equality [intro, simp] = +lemmas type_equality = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] - - -section \<open>Type families\<close> - -text "A type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property." - -abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)") - where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P(x) : U)" +\<close> end
\ No newline at end of file |