Skip to main content

The Cubical mode extends Agda with a variety of features from the CHM version of Cubical Type Theory. In particular, computational univalence and higher inductive types which hence gives computational meaning to Homotopy Type Theory and Univalent Foundations.

References:
Cubical mode - Agda