diff options
author | Josh Chen | 2018-08-30 00:51:48 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-30 00:51:48 +0200 |
commit | 2a2e8e46e0de6f99154a9421f75ae802557f22c7 (patch) | |
tree | 8dfcd36ddc5ea1da6609dbc06c2a273e36e1a1b6 /ex | |
parent | a7b46d4b0204571ba9124accebc84f77ae0bed26 (diff) |
Should write the correct rule for Ord_leq_min. Another exercise.
Diffstat (limited to 'ex')
-rw-r--r-- | ex/HoTT book/Ch1.thy | 12 |
1 files changed, 12 insertions, 0 deletions
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 |