Arend

Arend is a theorem prover based on Homotopy Type Theory. It natively supports higher inductive types and a version of cubical syntax. IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language.

Arend Features IntelliJ Arend Features

Recent Posts

Arend 1.0.0 released

The first version of Arend is released! It implements the following features: Path types based on the interval type. Higher inductive types, including ...