Proof Assistants (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

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:~~: Lean 2 has a HoTT mode, Lean 3 has a somewhat more hackish one~~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.