## 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: [Lean 2](https://github.com/leanprover/lean2) has a HoTT mode, [Lean 3](http://leanprover.github.io/) has a [somewhat more hackish one](https://github.com/gebner/hott3) * [Lean 2 & 3 HoTT libraries](https://github.com/leanprover/lean/wiki/HoTT-Library) * [Spectral sequences](https://github.com/cmu-phil/Spectral) (builds on Lean 2 library) ### Cubical type theories * [cubicaltt](https://github.com/mortberg/cubicaltt) * [redtt](http://github.com/redprl/redtt) * [yacctt](http://github.com/mortberg/yacctt) * [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]] category: proof assistants