aboutsummaryrefslogtreecommitdiff
path: root/ROOT
diff options
context:
space:
mode:
authorJosh Chen2019-02-04 11:53:47 +0100
committerJosh Chen2019-02-04 11:53:47 +0100
commit7a7e27f4a1efd69e9ab43b95d3c7ead61a743e55 (patch)
tree4ba31e925491f24c7fd23d59f6f3f74731b7a8e6 /ROOT
parent07d312b312c3058551353bcf403a1dc7c7c83311 (diff)
1. Change syntax to rely less on unicode/control symbols.
2. Begin work on object-level type inference and input syntax help.
Diffstat (limited to '')
-rw-r--r--ROOT3
1 files changed, 2 insertions, 1 deletions
diff --git a/ROOT b/ROOT
index cecdd32..b05d022 100644
--- a/ROOT
+++ b/ROOT
@@ -6,7 +6,8 @@ session HoTT = Pure +
hierarchy à la Russell.
Follows the development of the theory in
- The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics,
+ The Univalent Foundations Program,
+ Homotopy Type Theory: Univalent Foundations of Mathematics,
Institute for Advanced Study, (2013).
Available online at https://homotopytypetheory.org/book.