aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--EqualProps.thy1
-rw-r--r--ROOT10
-rw-r--r--ex/Book/Ch1.thy (renamed from ex/HoTT book/Ch1.thy)2
3 files changed, 11 insertions, 2 deletions
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/HoTT book/Ch1.thy b/ex/Book/Ch1.thy
index 263f43d..dfb1879 100644
--- a/ex/HoTT book/Ch1.thy
+++ b/ex/Book/Ch1.thy
@@ -1,5 +1,5 @@
(*
-Title: ex/HoTT book/Ch1.thy
+Title: ex/Book/Ch1.thy
Author: Josh Chen
Date: 2018