From 6857e783fa5cb91f058be322a18fb9ea583f2aad Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 11:38:54 +0200
Subject: Overhaul of the theory presentations. New methods in HoTT_Methods.thy
 for handling universes. Commit for release 0.1.0!

---
 ex/HoTT book/Ch1.thy | 47 +++++++++++++++++++++--------------------------
 1 file changed, 21 insertions(+), 26 deletions(-)

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

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