diff options
| -rw-r--r-- | Empty.thy | 2 | ||||
| -rw-r--r-- | HoTT_Base.thy | 17 |
2 files changed, 12 insertions, 7 deletions
@@ -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> |