diff options
author | Josh Chen | 2018-06-09 00:11:39 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-09 00:11:39 +0200 |
commit | 593faab277de53cbe2cb0c2feca5de307d9334ac (patch) | |
tree | e25f6868face9a2dc5c7db0cde9d0cd10381d466 /HoTT_Base.thy | |
parent | e12ef5b7216146513cbef0ed3c8d764e2e43c64e (diff) |
Reorganize code
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy new file mode 100644 index 0000000..9650c4c --- /dev/null +++ b/HoTT_Base.thy @@ -0,0 +1,52 @@ +(* Title: HoTT/HoTT_Base.thy + Author: Josh Chen + +Basic setup and definitions of a homotopy type theory object logic. +*) + +theory HoTT_Base + imports Pure + +begin + +section \<open>Basic definitions\<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." + +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) + + +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." + +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 + +lemmas type_equality [intro, simp] = + 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)" + +end
\ No newline at end of file |