aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-15 20:51:39 +0200
committerJosh Chen2018-09-15 20:51:39 +0200
commit515872533295e8464799467303fff923b52a2c01 (patch)
treeb3e716b20b152f734d42ed0ed5430d3460284727
parentae909b21905be847a2ce01388e34708c9d0246c0 (diff)
begin reorganizing
Diffstat (limited to '')
-rw-r--r--HoTT_Base.thy19
-rw-r--r--tests/Test.thy2
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>