# Homotopy Type Theory Proof Assistants (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

## 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

### 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.