Proof Assistants (Rev #2)

A partial list of proof assistants being used for formalizing homotopy type theory, and their libraries.

- Coq: use
`--indices-matter`

for HoTT - Agda: use
`--without-K`

for HoTT - Lean: Lean 2 has a HoTT mode, Lean 3 has a somewhat more hackish one
- Lean 2 & 3 HoTT libraries
- Spectral sequences (builds on Lean 2 library)

- Agda-flat: installation instructions

Revision on March 29, 2018 at 12:06:26 by Mike Shulman. See the history of this page for a list of all contributions to it.