pith. sign in

arxiv: 1406.0058 · v1 · pith:QEUWDECJnew · submitted 2014-05-31 · 🧮 math.AT · math.CT· math.LO

Univalent universes for elegant models of homotopy types

Denis-Charles Cisinski This is my paper
classification 🧮 math.AT math.CTmath.LO
keywords homotopytheorysetsunivalentcategoriestypesappartaxiom
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. The discrete homotopy hypothesis for directed graphs

    math.AT 2026-05 unverdicted novelty 7.0

    Localizing the category of directed graphs at cubical homotopy equivalences produces an ∞-category equivalent to the ∞-category of spaces.