Skip to content

Other proof assistants for HoTT

Rzk is not the first or the only proof assistant where it's possible to do (a variant of) homotopy type theory. Here is an incomplete list of such proof assistants and corresponding formalization libraries.

Agda

Agda is a dependently typed programming language (and also a proof assistant).

While by default Agda is not compatible with HoTT because of built-in Axiom K, it supports --without-K option, allowing to restore the compatibility with univalence. Some notable HoTT libraries in Agda include agda-unimath, HoTT-Agda.

Rzk's syntax for expressions is partially inspired by Agda. Rzk's (experimental) formatter is based on the code style accepted in emilyriehl/yoneda and rzk-lang/sHoTT projects, which comes largely from the code style of agda-unimath.

Agda is implemented in Haskell.

Arend

Arend is a theorem prover based on homotopy type theory with an interval type, making it similar to cubical type theories. Arend features a standard library at JetBrains/arend-lib.

Arend is developed by JetBrains, and is implemented in Java. It also features a plugin for IntelliJ IDEA turning it into an IDE for Arend.

Aya

Aya is an experimental cubical proof assistant, featuring type system features similar to Cubical Agda, redtt, and Arend. It also features overlapping and order-independent pattern matching, as well as some functional programming features similar to Haskell and Idris.

Aya is implemented in Java.

Formalizations in Aya?

I do not know of existing formalization libraries in Aya.

The red* family

cooltt, redtt, and RedPRL are a family of experimental proof assistants developed by the RedPRL Development Team.

There is a redtt mathematical library

The red* family of proof assistants is implemented in OCaml. The developers also have a related A.L.G.A.E. project, which aims to provide composable (OCaml) libraries that facilitate the construction of a usable proof assistant from a core type checker.

Coq

Coq is a mature proof assistant, based on the Calculus of Inductive Constructions. The original HoTT formalization, UniMath, initiated by Vladimir Voevodsky, is done in Coq and is maintained to this day by The UniMath Coordinating Committee. Other notable formalizations of HoTT in Coq include Coq-HoTT3

Coq is implemented in OCaml.

Cubical Agda

Cubical Agda is a mode extending Agda with a variety of features from Cubical Type Theory1 2.

Although technical a mode within Agda, it is probably best seen as a separate language. Cubical Agda (as well as other cubical proof assistants) supports a variant of extension types found in Rzk, albeit restricted to the use with cubical intervals.

Some notable formalizations in Cubical Agda include cubical and 1lab.

Cubical Agda as part of Agda is implemented in Haskell.

cubicaltt

cubicaltt is an experimental cubical proof assistant1 and a precursor to Cubical Agda.

Several formalizations in cubicaltt can be found at https://github.com/mortberg/cubicaltt/tree/master/examples.

cubicaltt is implemented in Haskell.

Lean

Lean is a teorem prover and a dependently typed programming language, based on the Calculus of Inductive Constructions. Similarly to Coq, Lean encourages heavy use of tactics and automation.

Lean 2, similarly to Agda, supported a mode without uniqueness of identity proofs (UIP), which allowed for HoTT formalizations. Hence, a formalization of HoTT in Lean 24 exists. However, since Lean 2 is not supported anymore, the formalization is also unmantained.

Lean 3 and 4 has dropped the mode that allowed (direct) HoTT formalization. However, the Ground Zero project attempts to formalize HoTT in Lean 4. The project makes use of the large elimination checker, ported from an unmaintained port of Lean 2 HoTT Library to Lean 3, which enables HoTT and non-HoTT scopes to coexist consistently (as the project authors believe). In particular, attempting to show UIP results in a type error under HoTT scope in the Ground Zero project.

Lean 2 and 3 are implemented in C++. Lean 4 is implemented in itself (and a bit of C++)!

  1. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2015.5 ↩↩

  2. Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). Association for Computing Machinery, New York, NY, USA, 255–264. https://doi.org/10.1145/3209108.3209197 ↩

  3. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. The HoTT library: a formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). Association for Computing Machinery, New York, NY, USA, 164–172. https://doi.org/10.1145/3018610.3018615 ↩

  4. Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_30 ↩