# nLab Arend

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# 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:

based on cubical type theory:

based on modal type theory:

projects for formalization of mathematics with proof assistants:

Other 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.