Arend implements a version of homotopy type theory with an interval type, which syntax is similar to cubical type theory. This implies several nice properties of path types and allows for a simple and clean definition of higher inductive types (including recursive ones). To learn more about homotopy features implemented in Arend, see Arend Features.

Arend has a powerful class system, which supports Haskell-style instance inference. Class inheritance can be used to define various hierarchies of (algebraic) structures. For a discussion of the class system, see Arend Features.

IntelliJ Arend

IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language. It has basic features such as syntax highlighting, “goto declaration”, and code folding. Moreover, IntelliJ Arend implements the following advanced features: