The univalence axiom for elegant Reedy presheaves

By Michael Shulman. 2013

64 citations recorded by the source corpus.

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.

Subfields: Algebra and Number Theory, Geometry and Topology, Mathematical Physics

View Paper: https://www.semanticscholar.org/paper/39b3d79c0c916db280277f3ce30d81213bfd889c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Algebra and Number Theory

1. Emily Riehl
2. Michael Shulman
3. Nicola Gambino
4. Christian Sattler
5. R. Haugseng
6. A. Mathew

In Geometry and Topology

1. Emily Riehl
2. Michael Shulman
3. Nicola Gambino
4. Christian Sattler
5. Dominic R. Verity
6. Richard Garner
7. R. Haugseng
8. A. Mathew

In Mathematical Physics

1. Emily Riehl
2. Nicola Gambino
3. Michael Shulman
4. Christian Sattler
5. Dominic R. Verity
6. Denis-Charles Cisinski
7. Richard Garner
8. Kathleen Ponto

Citations in the corpus

• The Frobenius condition, right properness, and uniform fibrations (2015, background): “ions ∂A→ yAand identity maps idyA: yA→ yA, and as morphisms commutative squares ∂A1 // yA2 yA1 y(d) //y A 2 8Note that our use of elegant Reedy presheaves is different from the one considered in [31] since here presheaves are valued in the category of sets, not in simplicial sets. 9This will be the”
• A type theory for synthetic ∞-categories (2017, methodology): “In particular, as shown in [27], it can be interpreted in the Reedy model structure on bisimplicial sets, also called simplicial spaces.”