From f9bbcffd4a45599c306815104dccb6b549b306ee Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 21:18:33 +0200
Subject: Add ROOT. No eta-contraction

---
 HoTT_Base.thy |  2 ++
 ROOT          | 18 ++++++++++++++++--
 2 files changed, 18 insertions(+), 2 deletions(-)

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
index 7e76f86..cecdd32 100644
--- a/ROOT
+++ b/ROOT
@@ -1,10 +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
+    HoTT_Methods
     "tests/Test"
     "ex/Methods"
     "ex/Synthesis"
-    "ex/Book/Ch1"
\ No newline at end of file
+    "ex/Book/Ch1"
-- 
cgit v1.2.3