aboutsummaryrefslogtreecommitdiff
path: root/ROOT
diff options
context:
space:
mode:
Diffstat (limited to 'ROOT')
-rw-r--r--ROOT18
1 files changed, 16 insertions, 2 deletions
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"