1 files changed, 24 insertions, 0 deletions
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"