Merge branch 'larsrh-topic/root'

4 files changed, 27 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/HoTT_Base.thy b/HoTT_Base.thy
index 2ad0ac5..69cc1b1 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -14,6 +14,8 @@ begin
 
 section \<open>Basic setup\<close>
 
+declare[[eta_contract=false]]
+
 typedecl t  \<comment> \<open>Type of object types and terms\<close>
 typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
 
diff --git a/ROOT b/ROOT
new file mode 100644
index 0000000..cecdd32
--- /dev/null
+++ b/ROOT
@@ -0,0 +1,24 @@
+chapter HoTT
+
+session HoTT = Pure +
+  description {*
+    Homotopy type theory based on intensional Martin-Löf type theory, with a cumulative universe
+    hierarchy à la Russell.
+    
+    Follows the development of the theory in
+    The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics,
+    Institute for Advanced Study, (2013).
+    Available online at https://homotopytypetheory.org/book.
+    
+    Author: Joshua Chen, University of Bonn (2018)
+  *}
+  sessions
+    "HOL-Eisbach"
+  theories
+    HoTT (global)
+    HoTT_Base
+    HoTT_Methods
+    "tests/Test"
+    "ex/Methods"
+    "ex/Synthesis"
+    "ex/Book/Ch1"
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