aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-12 06:34:03 +0200
committerJosh Chen2018-09-12 06:34:03 +0200
commit9cc9be2c6a86a6e31049c1f3512fa0b9806e03e9 (patch)
tree7e80bfea1bbf21eb3c50ef138209718347a67aba
parenta1afde729f1d9b2f930696b117cfaec827eaa178 (diff)
parent563510a1940024779c3e1f73df8c1b708eb0d949 (diff)
Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT
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