The univalence axiom for elegant Reedy presheaves

TL;DR

This paper proves that Voevodsky's univalence axiom holds in categories of simplicial presheaves on elegant Reedy categories, expanding its applicability to models of higher categories.

Contribution

It extends the validity of the univalence axiom to a broader class of categories, including bisimplicial sets and -spaces, with implications for higher category theory.

Findings

Univalence axiom holds in categories of simplicial presheaves on elegant Reedy categories.

Includes bisimplicial sets and -spaces as models.

Potential applications to homotopical models of higher categories.

Abstract

We show that Voevodsky's univalence axiom for intensional type theory is valid in categories of simplicial presheaves on elegant Reedy categories. In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and $\Theta_n$-spaces. This has potential applications to the study of homotopical models for higher categories.