aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT_Base.thy8
-rw-r--r--ex/HoTT book/Ch1.thy12
2 files changed, 18 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 269a3d9..be4899c 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -42,7 +42,7 @@ where
and
Ord_lt_monotone: "\<And>m n. m < n \<Longrightarrow> S(m) < S(n)"
and
- Ord_leq_min: "\<And>n. n \<le> n"
+ Ord_leq_min: "\<And>n. O \<le> n"
and
Ord_leq_monotone: "\<And>m n. m \<le> n \<Longrightarrow> S(m) \<le> S(n)"
@@ -57,7 +57,11 @@ where
U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U(i): U(j)"
and
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>
+
+text "
+ The rule \<open>U_cumulative\<close> is very unsafe: if used as-is it will usually lead to an infinite rewrite loop!
+ It should be instantiated with the right ordinals \<open>i\<close> and \<open>j\<close> before being applied.
+"
section \<open>Type families\<close>
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index d5f05dd..a577fca 100644
--- a/ex/HoTT book/Ch1.thy
+++ b/ex/HoTT book/Ch1.thy
@@ -40,4 +40,16 @@ proof (rule Sum_elim[where ?p=p])
qed (derive lems: assms)
+section \<open>Exercises\<close>
+
+text "Exercise 1.13"
+
+abbreviation "not" ("\<not>'(_')") where "\<not>(A) \<equiv> A \<rightarrow> \<zero>"
+
+text "This proof requires the use of universe cumulativity."
+
+proposition assumes "A: U(i)" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`inl(a))): \<not>(\<not>(A + \<not>(A)))"
+by (derive lems: assms U_cumulative[where ?A=\<zero> and ?i=O and ?j=i])
+
+
end