Proof Assistants (changes)

Showing changes from revision #4 to #5:
Added | ~~Removed~~ | ~~Chan~~ged

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

- Coq: use

for HoTT~~--indices-matter~~-indices-matter - 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 November 18, 2019 at 09:40:21. See the history of this page for a list of all contributions to it.