From d8699451025a3bd5e8955e07fa879ed248418949 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 16 Aug 2018 16:28:50 +0200
Subject: Some comments and reorganization

---
 ex/HoTT Book/Ch1.thy | 37 -------------------------------------
 ex/HoTT book/Ch1.thy | 44 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 37 deletions(-)
 delete mode 100644 ex/HoTT Book/Ch1.thy
 create mode 100644 ex/HoTT book/Ch1.thy

(limited to 'ex')

diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT Book/Ch1.thy
deleted file mode 100644
index 84a5cf4..0000000
--- a/ex/HoTT Book/Ch1.thy	
+++ /dev/null
@@ -1,37 +0,0 @@
-theory Ch1
-  imports "../../HoTT"
-begin
-
-chapter \<open>HoTT Book, Chapter 1\<close>
-
-section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
-
-text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor."
-
-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>"
-
-text "Proof by induction on \<open>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)+
-
-  qed (derive lems: assms asm)
-
-qed (derive lems: assms)
-
-
-end
\ No newline at end of file
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
new file mode 100644
index 0000000..65de875
--- /dev/null
+++ b/ex/HoTT book/Ch1.thy	
@@ -0,0 +1,44 @@
+(*  Title:  HoTT/ex/HoTT book/Ch1.thy
+    Author: Josh Chen
+    Date:   Aug 2018
+
+A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
+*)
+
+theory Ch1
+  imports "../../HoTT"
+begin
+
+chapter \<open>HoTT Book, Chapter 1\<close>
+
+section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
+
+text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor."
+
+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>"
+
+text "Proof by induction on \<open>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)+
+
+  qed (derive lems: assms asm)
+
+qed (derive lems: assms)
+
+
+end
\ No newline at end of file
-- 
cgit v1.2.3