1 files changed, 21 insertions, 22 deletions
diff --git a/ROOT b/ROOT
index b05d022..e62fa06 100644
--- a/ROOT
+++ b/ROOT
@@ -1,25 +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)
-  *}
+session Spartan in "spartan/theories" = Pure +
+  description "
+    Spartan type theory: a minimal dependent type theory based on
+    intensional Martin-Löf type theory with cumulative Russell-style universes,
+    Pi, Sigma and identity types.
+  "
   sessions
     "HOL-Eisbach"
   theories
-    HoTT (global)
-    HoTT_Base
-    HoTT_Methods
-    "tests/Test"
-    "ex/Methods"
-    "ex/Synthesis"
-    "ex/Book/Ch1"
+    Spartan (global)
+    Identity
+    Equivalence
+
+session HoTT in hott = Spartan +
+  description "
+    Homotopy type theory, following the development in
+      The Univalent Foundations Program,
+      Homotopy Type Theory: Univalent Foundations of Mathematics,
+      Institute for Advanced Study, (2013).
+      Available online at https://homotopytypetheory.org/book.
+  "
+  theories
+    Basic_Types
+    Nat