aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-07-16 16:20:15 +0200
committerJosh Chen2020-07-16 16:20:15 +0200
commit2a2fa1e4c643b73165af030dc3b6128886f7b654 (patch)
tree82f64dd327d05c32cecb22b05ae705906f2faf88
parent79659cb0edf1eea026a93955403a33a1f38f6123 (diff)
update readme
-rw-r--r--README.md4
1 files changed, 2 insertions, 2 deletions
diff --git a/README.md b/README.md
index 6686e0b..30e1237 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,9 @@
# Isabelle/HoTT
Isabelle/HoTT is an experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in the [Isabelle](https://isabelle.in.tum.de/) interactive theorem prover.
-It largely follows the development of the theory in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/), but aims to be general enough to support cubical and other kinds of homotopy type theories.
+It largely follows the development of the theory in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/), but aims to be general enough to eventually support cubical and other kinds of homotopy type theories.
-Work is slowly ongoing to develop the logic into a fully-featured framework in which one can formulate and prove mathematical statements, in the style of the univalent foundations school.
+Work is slowly ongoing to develop the logic into a fully-featured proof environment in which one can formulate and prove mathematical statements, in the style of the univalent foundations school.
While Isabelle has provided support for object logics based on Martin-Löf type theory since the beginning, these have largely been ignored in favor of Isabelle/HOL.
Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle/Pure.