#
Homotopy Type Theory

Proof Assistants (Rev #1)

## Proof Assistants

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

### Book HoTT

- 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

### Cubical type theories

### Modal type theories

### Other

Revision on March 25, 2018 at 10:53:41 by
Mike Shulman.
See the history of this page for a list of all contributions to it.