blob: 92464c7760902ce2bfa1053b0e99ba03683aa7f0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
# 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
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.
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`.
## License
MIT
|
