Homotopy Type Theory
Proof Assistants

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
  • HoTT/Coq library
• Agda: use --without-K for HoTT
  • HoTT/Agda library
• 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)

Cubical type theories

• cubicaltt
• redtt
• yacctt
• RedPRL
• Cubical Agda
  • library and demos

Modal type theories

• Agda-flat: installation instructions

Other

• Andromeda

category: proof assistants