diff options
| -rw-r--r-- | HoTT_Base.thy | 19 | ||||
| -rw-r--r-- | tests/Test.thy | 2 |
2 files changed, 11 insertions, 10 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1110e14..8ea767f 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,11 +1,12 @@ (* Title: HoTT/HoTT_Base.thy - Author: Josh Chen + Author: Joshua Chen Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. *) theory HoTT_Base - imports Pure +imports Pure + begin @@ -13,7 +14,7 @@ section \<open>Foundational definitions\<close> text "Meta syntactic type for object-logic types and terms." -typedecl Term +typedecl t section \<open>Judgments\<close> @@ -23,19 +24,19 @@ text " For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it. " -judgment has_type :: "[Term, Term] \<Rightarrow> prop" ("(3_:/ _)" [0, 0] 1000) +judgment hastype :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)") section \<open>Universe hierarchy\<close> -text "Finite meta-ordinals to index the universes." +text "Meta-numerals to index the universes." -typedecl Ord +typedecl ord axiomatization - O :: Ord and - S :: "Ord \<Rightarrow> Ord" ("S_" [0] 1000) and - lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<-" 999) + O :: ord and + S :: "ord \<Rightarrow> ord" ("S_") and + lt :: "[ord, ord] \<Rightarrow> prop" (infix "<-" 999) where Ord_min: "\<And>n. O <- S(n)" and diff --git a/tests/Test.thy b/tests/Test.thy index b0eb87a..de65dbd 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -23,7 +23,7 @@ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close> -section \<open>\<Pi>-type\<close> +section \<open>\<Prod>-type\<close> subsection \<open>Typing functions\<close> |