diff options
author | Josh Chen | 2018-07-03 17:06:58 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-03 17:06:58 +0200 |
commit | 9ffa5ed2a972db4ae6274a7852de37945a32ab0e (patch) | |
tree | d44c0877ac0316834c3e566728608f686aaa38be /HoTT_Base.thy | |
parent | 14a5e50ab3ed54767a4432333642e9069ffa9109 (diff) |
Rewrote methods: wellformed now two lines, uses named theorems. New, more powerful derive method. Used these to rewrite proofs.
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 561dbe6..e5c0776 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -11,13 +11,14 @@ begin section \<open>Setup\<close> -text "Set up type checking routines, proof methods etc." +text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments." +named_theorems wellform section \<open>Metalogical definitions\<close> text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms. -We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ''\<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 @@ -35,7 +36,7 @@ consts text "The following fact is used to make explicit the assumption of well-formed contexts." axiomatization where - inhabited_implies_type [intro, elim]: "\<And>a A. a : A \<Longrightarrow> A : U" + inhabited_implies_type [intro, elim, wellform]: "\<And>a A. a : A \<Longrightarrow> A : U" section \<open>Type families\<close> @@ -47,7 +48,7 @@ type_synonym Typefam = "Term \<Rightarrow> Term" 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 code, and is for the moment not really crucial." +\<comment> \<open>There is an obvious generalization to multivariate type families, but implementing such an abbreviation would probably involve writing ML code, and is for the moment not really crucial.\<close> end
\ No newline at end of file |