diff options
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index a0078fa..561dbe6 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -17,7 +17,7 @@ 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. -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 @@ -32,6 +32,8 @@ consts is_a_type :: "Term \<Rightarrow> prop" ("(1_ :/ U)" [0] 1000) is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) +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" |