aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-11 19:27:57 +0200
committerGitHub2018-09-11 19:27:57 +0200
commit563510a1940024779c3e1f73df8c1b708eb0d949 (patch)
tree54839c7bda1bd1fd5d6b9fa9e9152745cfb51e37
parentd7b9fc814d0fcb296156143a5d9bc3f5d9ad9ad1 (diff)
Update README.md
Diffstat (limited to '')
-rw-r--r--README.md10
1 files changed, 7 insertions, 3 deletions
diff --git a/README.md b/README.md
index 68ede63..d557f3e 100644
--- a/README.md
+++ b/README.md
@@ -4,15 +4,19 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or
### Installation & Usage
-Clone the contents of this repository into `<Isabelle root directory>/src/Isabelle-HoTT`.
+Clone or copy the contents of this repository into `<Isabelle root directory>/src/Isabelle-HoTT`.
To use, set Isabelle's prover to Pure in the Theories panel, and import `HoTT`.
+### Some comments on the implementation
+
+The implementation in the `master` branch is polymorphic without type annotations, and as such has some differences with the standard theory as presented in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/).
+
### Collaboration
-I've been flying solo on this library as part of my Masters project, and there are very many improvements and developments that have yet to be implemented, so ***collaborators are welcome!***
+I've been flying solo on this library as part of my Masters project, and there are very many improvements and developments that have yet to be implemented, so **collaborators are welcome!**
-If you're interested in working together on any part of this do drop me a line at `joshua DOT chen AT uni-bonn DOT de`.
+If you're interested in working together on any part of this library do drop me a line at `joshua DOT chen AT uni-bonn DOT de`.
### License