## Proof Assistants A partial list of proof assistants being used for formalizing homotopy type theory, and their libraries. ### Book HoTT * [Coq](http://coq.inria.fr): use `--indices-matter` for HoTT * [HoTT/Coq library](http://github.com/HoTT/HoTT) * [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php): use `--without-K` for HoTT * [HoTT/Agda library](https://github.com/HoTT/HoTT-Agda) * [Lean](http://leanprover.github.io/): Lean 2 has a HoTT mode, Lean 3 has a somewhat more hackish one * [Lean 2 & 3 HoTT libraries](https://github.com/leanprover/lean/wiki/HoTT-Library) ### Cubical type theories * [cubicaltt](https://github.com/mortberg/cubicaltt) * [RedPRL](http://www.redprl.org/en/latest/) * [Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) * [library and demos](https://github.com/Saizan/cubical-demo) ### Modal type theories * Agda-flat: [installation instructions](http://www.cl.cam.ac.uk/~amp12/agda/internal-universes/code/agda-flat/install.txt) ### Other * [Andromeda](http://www.andromeda-prover.org/) [[!redirects Libraries]]