The univalence axiom in cubical sets

TL;DR

This paper demonstrates that Voevodsky's univalence axiom is valid within the symmetric cubical sets model of type theory, supporting key type-theoretic constructs in a constructive setting.

Contribution

It establishes a constructive model of type theory with univalence in symmetric cubical sets, including identity types and dependent types.

Findings

Univalence axiom holds in symmetric cubical sets

Model supports dependent products and sums

Constructive formulation of the model

Abstract

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 type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.