diff options
Diffstat (limited to '')
| -rw-r--r-- | README.md | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -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 |