# Isabelle/HoTT
An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in the interactive theorem prover [Isabelle](https://isabelle.in.tum.de/).

## Installation
Clone the contents of this repository into `<Isabelle root directory>/src/HoTT`.

## Usage
Set Isabelle's prover to Pure in the Theories panel, and import `HoTT`.

## Collaboration
Collaborators welcome!

I've been working on this library as part of my Masters project, and there are very many improvements and developments that have yet to be implemented.
If you're interested in working together on any part of this do drop me a line!

## License
MIT