aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-08-30 00:45:08 +0200
committerJosh Chen2018-08-30 00:45:08 +0200
commita7b46d4b0204571ba9124accebc84f77ae0bed26 (patch)
tree5b96f1637659816097c12cdeb3b518e6f7fe0034
parent5193d4dd1ebef7fa000489710ff138ab98876c52 (diff)
Add leq relation to meta-ordinals, it helps with proofs
-rw-r--r--Empty.thy2
-rw-r--r--HoTT_Base.thy17
2 files changed, 12 insertions, 7 deletions
diff --git a/Empty.thy b/Empty.thy
index 1b339ba..8f5cc8c 100644
--- a/Empty.thy
+++ b/Empty.thy
@@ -17,7 +17,7 @@ axiomatization
Empty :: Term ("\<zero>") and
indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)")
where
- Empty_form: "\<zero> : U(O)"
+ Empty_form: "\<zero>: U(O)"
and
Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 1110e14..269a3d9 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -35,13 +35,18 @@ typedecl Ord
axiomatization
O :: Ord and
S :: "Ord \<Rightarrow> Ord" ("S_" [0] 1000) and
- lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<-" 999)
+ lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<" 999) and
+ leq :: "[Ord, Ord] \<Rightarrow> prop" (infix "\<le>" 999)
where
- Ord_min: "\<And>n. O <- S(n)"
+ Ord_lt_min: "\<And>n. O < S(n)"
and
- Ord_monotone: "\<And>m n. m <- n \<Longrightarrow> S(m) <- S(n)"
+ Ord_lt_monotone: "\<And>m n. m < n \<Longrightarrow> S(m) < S(n)"
+and
+ Ord_leq_min: "\<And>n. n \<le> n"
+and
+ Ord_leq_monotone: "\<And>m n. m \<le> n \<Longrightarrow> S(m) \<le> S(n)"
-lemmas Ord_rules [intro] = Ord_min Ord_monotone
+lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_monotone Ord_leq_min Ord_leq_monotone
\<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close>
text "Define the universe types."
@@ -49,9 +54,9 @@ text "Define the universe types."
axiomatization
U :: "Ord \<Rightarrow> Term"
where
- U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i): U(j)"
+ U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U(i): U(j)"
and
- U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i <- j\<rbrakk> \<Longrightarrow> A: U(j)"
+ U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i \<le> j\<rbrakk> \<Longrightarrow> A: U(j)"
\<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close>