diff options
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 40 |
1 files changed, 13 insertions, 27 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9b422c4..7794601 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -2,7 +2,7 @@ Author: Josh Chen Date: Jun 2018 -Basic setup and definitions of a homotopy type theory object logic. +Basic setup and definitions of a homotopy type theory object logic without universes. *) theory HoTT_Base @@ -18,16 +18,23 @@ 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''." +We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''." typedecl Term section \<open>Judgments\<close> +text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> separately, in contrast to the HoTT book where the latter is considered an instance of the former. + +For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it." + consts -is_a_type :: "Term \<Rightarrow> prop" ("(1_ :/ U)" [0] 1000) -is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) + is_a_type :: "Term \<Rightarrow> prop" ("(1_ :/ U)" [0] 1000) + is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) + +axiomatization where + inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U" section \<open>Type families\<close> @@ -36,31 +43,10 @@ text "A (one-variable) type family is a meta lambda term \<open>P :: Term \<Righ type_synonym Typefam = "Term \<Rightarrow> Term" -abbreviation is_type_family :: "[Typefam, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)") +abbreviation (input) 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 "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" - shows "B : U" using assms by simp - -theorem equal_type_element: - assumes "A \<equiv> B" and "x : A" - shows "x : B" using assms by simp +text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML code, and is for the moment not really crucial." -lemmas type_equality = - equal_types - equal_types[rotated] - equal_type_element - equal_type_element[rotated] -\<close> end
\ No newline at end of file |