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

category: proof assistants