Proof Assistants

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

Last revised on August 25, 2018 at 19:40:11. See the history of this page for a list of all contributions to it.