diff options
author | Josh Chen | 2018-05-10 19:13:05 +0200 |
---|---|---|
committer | Josh Chen | 2018-05-10 19:13:05 +0200 |
commit | 5b217a7eb36906eabdcb6ec626a2d02e0f94c308 (patch) | |
tree | af22f3e27f96d533370fa368f7c742c165dee3d9 /HoTT.thy | |
parent | 502e5d2526e59c9b5d98fbbaef93b5fbc0c3011d (diff) |
Decided to go with no explicit type declarations in object-lambda expressions. Everything in the proof stuff is working at the moment.
Diffstat (limited to 'HoTT.thy')
-rw-r--r-- | HoTT.thy | 39 |
1 files changed, 25 insertions, 14 deletions
@@ -3,32 +3,42 @@ imports Pure begin section \<open>Setup\<close> - -(* ML files, routines and setup should probably go here *) +text \<open> +For ML files, routines and setup. +\<close> section \<open>Basic definitions\<close> - text \<open> A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms. - For now we do not implement universes, but simply follow the informal notation in the HoTT book. -\<close> -(* Actually unsure if a single meta-type suffices... *) +\<close> (* Actually unsure if a single meta-type suffices... *) typedecl Term subsection \<open>Judgements\<close> - consts is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)") (* Add precedences when I figure them out! *) is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop" ("(_ : _)") subsection \<open>Basic axioms\<close> +subsubsection \<open>Definitional equality\<close> +text\<open> +We take the meta-equality \<equiv>, defined by the Pure framework for any of its terms, +and use it additionally for definitional/judgmental equality of types and terms in our theory. -axiomatization -where - inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" and - equal_types: "\<And>A B x. A \<equiv> B \<Longrightarrow> x : A \<Longrightarrow> x : B" +Note that the Pure framework already provides axioms and results for the various properties of \<equiv>, +which we make use of and extend where necessary. +\<close> + + +theorem DefEq_symmetry: "\<And>A B. A \<equiv> B \<Longrightarrow> B \<equiv> A" + by (rule Pure.symmetric) + +subsubsection \<open>Type-related properties\<close> + +axiomatization where + equal_types: "\<And>A B x. \<lbrakk>A \<equiv> B; x : A\<rbrakk> \<Longrightarrow> x : B" and + inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" subsection \<open>Basic types\<close> @@ -41,7 +51,8 @@ Same for the nondependent product below. axiomatization Function :: "Term \<Rightarrow> Term \<Rightarrow> Term" (infixr "\<rightarrow>" 10) and - lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 10) and (* precedence! *) + lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 10) and + (* Is bold lambda already used by something else? Proof transformers in Pure maybe?... *) appl :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(_`_)") where Function_form: "\<And>A B. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<rightarrow>B : U" and @@ -62,8 +73,8 @@ where Product_comp: "\<And>A B C g a b. \<lbrakk>C : U; g : A\<rightarrow>B\<rightarrow>C; a : A; b : B\<rbrakk> \<Longrightarrow> rec_Product(A,B,C,g)`(a,b) \<equiv> (g`a)`b" \<comment> \<open>Projection onto first component\<close> -definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1'(_,_'))") where - "proj1(A,B) \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)" +definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1\<langle>_,_\<rangle>)") where + "proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)" subsubsection \<open>Empty type\<close> |