Decomposing the Univalence Axiom

TL;DR

This paper offers a new way to understand Voevodsky's univalence axiom by decomposing it into simpler, more verifiable axioms, especially relevant for models based on cubical sets, and addresses an open problem in type theory.

Contribution

It introduces a novel decomposition of the univalence axiom into simpler axioms, facilitating verification in cubical set models and advancing understanding in univalent type theory.

Findings

Decomposition of univalence into simpler axioms.

Enhanced verification in cubical set models.

Relevance to an open problem in type theory.

Abstract

This paper investigates Voevodsky's univalence axiom in intensional Martin-L\"of type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.