From f07e0e2349a222130209ada9c029eea3d1fe8144 Mon Sep 17 00:00:00 2001
From: Lars Hupel
Date: Tue, 18 Sep 2018 16:52:08 +0200
Subject: add ROOT file

---
 EqualProps.thy       |  1 -
 ROOT                 | 10 ++++++++++
 ex/Book/Ch1.thy      | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 ex/HoTT book/Ch1.thy | 50 --------------------------------------------------
 4 files changed, 60 insertions(+), 51 deletions(-)
 create mode 100644 ROOT
 create mode 100644 ex/Book/Ch1.thy
 delete mode 100644 ex/HoTT book/Ch1.thy

diff --git a/EqualProps.thy b/EqualProps.thy
index abb2623..f7a8d91 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -117,7 +117,6 @@ proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
   fix x assume "x: A"
   show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r"
   \<comment> \<open>This requires substitution of *propositional* equality. \<close>
-  sorry
   oops
 
 
diff --git a/ROOT b/ROOT
new file mode 100644
index 0000000..7e76f86
--- /dev/null
+++ b/ROOT
@@ -0,0 +1,10 @@
+session HoTT = Pure +
+  sessions
+    "HOL-Eisbach"
+  theories
+    HoTT_Base
+    HoTT
+    "tests/Test"
+    "ex/Methods"
+    "ex/Synthesis"
+    "ex/Book/Ch1"
\ No newline at end of file
diff --git a/ex/Book/Ch1.thy b/ex/Book/Ch1.thy
new file mode 100644
index 0000000..dfb1879
--- /dev/null
+++ b/ex/Book/Ch1.thy
@@ -0,0 +1,50 @@
+(*
+Title:  ex/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"
+
+begin
+
+chapter \<open>HoTT Book, Chapter 1\<close>
+
+section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
+
+paragraph \<open>Propositional uniqueness principle.\<close>
+
+schematic_goal
+  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 \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
+
+proof (rule Sum_elim[where ?p=p])
+  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>
+
+paragraph \<open>Exercise 1.13\<close>
+
+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)
+
+
+end
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
deleted file mode 100644
index 263f43d..0000000
--- a/ex/HoTT book/Ch1.thy	
+++ /dev/null
@@ -1,50 +0,0 @@
-(*
-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"
-
-begin
-
-chapter \<open>HoTT Book, Chapter 1\<close>
-
-section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
-
-paragraph \<open>Propositional uniqueness principle.\<close>
-
-schematic_goal
-  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 \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
-
-proof (rule Sum_elim[where ?p=p])
-  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>
-
-paragraph \<open>Exercise 1.13\<close>
-
-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)
-
-
-end
-- 
cgit v1.2.3