From b815a897c04350f6b2335a15e30844316a5cce9e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 15 Oct 2019 23:13:00 +0200 Subject: Update README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index f254a8a..edc5399 100644 --- a/README.md +++ b/README.md @@ -16,6 +16,7 @@ In its current state it is best viewed as a formalization of HoTT within Isabell 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. 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. +**Update (15 Oct 2019)**: Framework development currently [here](https://github.com/jaycech3n/Isabelle-Spartan). ### License -- cgit v1.2.3 From 32dc5b962b171a180568c1352a4a3301029605a1 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 29 Oct 2019 11:51:26 +0100 Subject: Update README.md --- README.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index edc5399..a095173 100644 --- a/README.md +++ b/README.md @@ -2,6 +2,9 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). +**Update [15 Oct 2019]**: +Convenience and readability of formalizations in the library is taking a hit as we move to the limits of the currently available functionality in Isabelle, so for the moment development has moved [here](https://github.com/jaycech3n/Isabelle-Spartan), in order to first build more necessary automation and improve the framework. + ### Usage The default entry point for the logic is `HoTT`, import this to load everything else. @@ -16,7 +19,8 @@ In its current state it is best viewed as a formalization of HoTT within Isabell 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. 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. -**Update (15 Oct 2019)**: Framework development currently [here](https://github.com/jaycech3n/Isabelle-Spartan). + +A writeup of some theoretical considerations in this implementation is in my [Masters thesis](https://joshchen.io/assets/ms_thesis_submitted.pdf). ### License -- cgit v1.2.3 From d7ae8044e7413f8bb0bc25d4a903b8fc206d7611 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 29 Oct 2019 11:52:02 +0100 Subject: Update README.md --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index a095173..12c06fa 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,8 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). **Update [15 Oct 2019]**: -Convenience and readability of formalizations in the library is taking a hit as we move to the limits of the currently available functionality in Isabelle, so for the moment development has moved [here](https://github.com/jaycech3n/Isabelle-Spartan), in order to first build more necessary automation and improve the framework. +Convenience and readability of formalizations in the library is taking a hit as we move to the limits of the currently available functionality in Isabelle. +Hence for the moment development has moved [here](https://github.com/jaycech3n/Isabelle-Spartan) in order to first build more necessary automation and improve the framework. ### Usage -- cgit v1.2.3 From 326475c661337d7511fbcfa126e66bc1f1bd83f6 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 29 Oct 2019 14:58:58 +0100 Subject: Update README.md --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 12c06fa..0837880 100644 --- a/README.md +++ b/README.md @@ -2,9 +2,9 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). -**Update [15 Oct 2019]**: -Convenience and readability of formalizations in the library is taking a hit as we move to the limits of the currently available functionality in Isabelle. -Hence for the moment development has moved [here](https://github.com/jaycech3n/Isabelle-Spartan) in order to first build more necessary automation and improve the framework. +**Update [Oct 2019]**: +Convenience and readability of formalizations in this library is taking a hit as we approach the limit of the functionality that's currently available in Isabelle. +Development is thus, for the moment, moving [here](https://github.com/jaycech3n/Isabelle-Spartan) to first build more automation and improve the framework. ### Usage -- cgit v1.2.3 From b4faf763660070e882f9f09985238e0fe4f47ad3 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 29 Nov 2019 16:52:10 +0100 Subject: Change link --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0837880..c1a30c2 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ Work is slowly ongoing to develop the logic into a fully-featured framework in w 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. -A writeup of some theoretical considerations in this implementation is in my [Masters thesis](https://joshchen.io/assets/ms_thesis_submitted.pdf). +A writeup of some theoretical considerations in this implementation is in my [Masters thesis](https://arxiv.org/abs/1911.00399). ### License -- cgit v1.2.3 From 1d99fa1fb0e257244aabcb3f63ae7c5ca13555ab Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 24 Jan 2020 16:52:09 +0100 Subject: Update README.md --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index c1a30c2..c33682a 100644 --- a/README.md +++ b/README.md @@ -2,9 +2,9 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). -**Update [Oct 2019]**: -Convenience and readability of formalizations in this library is taking a hit as we approach the limit of the functionality that's currently available in Isabelle. -Development is thus, for the moment, moving [here](https://github.com/jaycech3n/Isabelle-Spartan) to first build more automation and improve the framework. +### Update [Oct 2019] +Convenience and readability of formalizations in this library is taking a hit as we approach the limit of pre-existing functionality available in Isabelle. +Development is thus, for the moment, moving to [Isabelle/Spartan](https://github.com/jaycech3n/Isabelle-Spartan) to build more automation and improve the framework. ### Usage -- cgit v1.2.3 From fc2a739f92a26c9b5d53e529a74cc95525580d63 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 24 Jan 2020 16:52:45 +0100 Subject: Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c33682a..6338e6d 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). -### Update [Oct 2019] +### UPDATE, Oct 2019 Convenience and readability of formalizations in this library is taking a hit as we approach the limit of pre-existing functionality available in Isabelle. Development is thus, for the moment, moving to [Isabelle/Spartan](https://github.com/jaycech3n/Isabelle-Spartan) to build more automation and improve the framework. -- cgit v1.2.3 From 438e2100bcf7355a6e18d696c2c7a8baadf856d5 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 24 Jan 2020 16:58:02 +0100 Subject: Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 6338e6d..a93b834 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or ### UPDATE, Oct 2019 Convenience and readability of formalizations in this library is taking a hit as we approach the limit of pre-existing functionality available in Isabelle. -Development is thus, for the moment, moving to [Isabelle/Spartan](https://github.com/jaycech3n/Isabelle-Spartan) to build more automation and improve the framework. +Development has thus, for the moment, moved to [Isabelle/Spartan](https://github.com/jaycech3n/Isabelle-Spartan) to build more automation and improve the framework. ### Usage -- cgit v1.2.3 From 045fc390b7fba9e0f0573368403af9e50694b60e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 24 Jan 2020 17:01:12 +0100 Subject: make development shift really obvious --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index a93b834..a65aab1 100644 --- a/README.md +++ b/README.md @@ -2,8 +2,8 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). -### UPDATE, Oct 2019 -Convenience and readability of formalizations in this library is taking a hit as we approach the limit of pre-existing functionality available in Isabelle. +## Caveat lector +The convenience and readability of formalizations in this library is taking a hit as we approach the limit of pre-existing functionality available in Isabelle. Development has thus, for the moment, moved to [Isabelle/Spartan](https://github.com/jaycech3n/Isabelle-Spartan) to build more automation and improve the framework. ### Usage -- cgit v1.2.3