aboutsummaryrefslogtreecommitdiff
path: root/ROOT
diff options
context:
space:
mode:
authorJosh Chen2018-09-18 21:18:33 +0200
committerJosh Chen2018-09-18 21:18:33 +0200
commitf9bbcffd4a45599c306815104dccb6b549b306ee (patch)
treefe25a144dfac0727a71371176d3f63927407d2d9 /ROOT
parentf07e0e2349a222130209ada9c029eea3d1fe8144 (diff)
Add ROOT. No eta-contraction
Diffstat (limited to '')
-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"