# Isabelle/HoTT [![DOI](https://zenodo.org/badge/134523964.svg)](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