2 papers
cs.LO2018
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…
math.LO2017
The univalence axiom in cubical sets
Marc Bezem, Thierry Coquand, Simon Huber
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. We will also discuss Swan's construction of the identity t…