blob: d6860b128d8c36d97ebf69717fd268d2d2320efb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
# Isabelle/HoTT [](https://zenodo.org/badge/latestdoi/134523964)
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/).
### Usage
The default entry point for the logic is `HoTT`, which loads everything else.
You can also load theories selectively, in this case,`HoTT_Base` is required and `HoTT_Methods` is helpful.
### License
GNU LGPLv3
|
