On Higher Inductive Types in Cubical Type Theory

Thierry Coquand, Simon Huber, Anders Mörtberg

Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles…