aboutsummaryrefslogtreecommitdiff
path: root/ex/HoTT book
diff options
context:
space:
mode:
Diffstat (limited to 'ex/HoTT book')
-rw-r--r--ex/HoTT book/Ch1.thy47
1 files changed, 21 insertions, 26 deletions
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index a577fca..263f43d 100644
--- a/ex/HoTT book/Ch1.thy
+++ b/ex/HoTT book/Ch1.thy
@@ -1,55 +1,50 @@
-(* Title: HoTT/ex/HoTT book/Ch1.thy
- Author: Josh Chen
+(*
+Title: ex/HoTT book/Ch1.thy
+Author: Josh Chen
+Date: 2018
A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
*)
theory Ch1
- imports "../../HoTT"
+imports "../../HoTT"
+
begin
chapter \<open>HoTT Book, Chapter 1\<close>
-section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
+section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
-text "Propositional uniqueness principle:"
+paragraph \<open>Propositional uniqueness principle.\<close>
schematic_goal
- assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
- shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>"
+ assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x"
+ shows "?a: p =[\<Sum>x:A. B x] <fst p, snd p>"
-text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:"
+text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
proof (rule Sum_elim[where ?p=p])
- text "We just need to prove the base case; the rest will be taken care of automatically."
-
- fix x y assume asm: "x: A" "y: B(x)" show
- "refl(<x,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>"
- proof (subst (0 1) comp)
- text "
- The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> have appropriate types.
- The automatic proof methods have trouble picking the appropriate types, so we state them explicitly,
- "
- show "x: A" and "y: B(x)" by (fact asm)+
-
- text "...twice, once each for the substitutions of \<open>fst\<close> and \<open>snd\<close>."
- show "x: A" and "y: B(x)" by (fact asm)+
+ text \<open>We prove the base case.\<close>
+ fix x y assume asm: "x: A" "y: B x" show "refl <x,y>: <x,y> =[\<Sum>x:A. B x] <fst <x,y>, snd <x,y>>"
+ proof compute
+ show "x: A" and "y: B x" by (fact asm)+ \<comment> \<open>Hint the correct types.\<close>
+ text \<open>And now @{method derive} takes care of the rest.
+\<close>
qed (derive lems: assms asm)
-
qed (derive lems: assms)
section \<open>Exercises\<close>
-text "Exercise 1.13"
+paragraph \<open>Exercise 1.13\<close>
-abbreviation "not" ("\<not>'(_')") where "\<not>(A) \<equiv> A \<rightarrow> \<zero>"
+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])
+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)
end