From 2a2e8e46e0de6f99154a9421f75ae802557f22c7 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 30 Aug 2018 00:51:48 +0200
Subject: Should write the correct rule for Ord_leq_min. Another exercise.

---
 ex/HoTT book/Ch1.thy | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'ex/HoTT book/Ch1.thy')

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
-- 
cgit v1.2.3