Univalent universes for elegant models of homotopy types

TL;DR

This paper constructs a univalent universe within certain model categories, enabling the interpretation of intensional type theory with the univalent axiom across various models like cubical and cellular sets.

Contribution

It introduces a univalent universe in model categories derived from Grothendieck's test categories, broadening the interpretative frameworks for homotopy type theory.

Findings

Univalent universe constructed in model categories from test categories

Interpretation of type theory with univalence in cubical and cellular sets

Extension of homotopy-theoretic models for type theory

Abstract

We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for instance that, appart from the homotopy theory of simplicial sets, intensional type theory with the univalent axiom can be interpreted in the homotopy theory of cubical sets (with connections or not), or of Joyal's cellular sets.