Contents

Contents

Idea

Arend is a proof assistant system for homotopy type theory with native support for higher inductive types and some cubical type theory.

proof assistants:

based on plain type theory/set theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:

References

Created on September 12, 2019 at 02:48:21. See the history of this page for a list of all contributions to it.