(Link)

Author: Michael Shulman (University of San Diego)

Reference: Shulman, Michael. “All (∞,1)-toposes have strict univalent universes.” arXiv preprint arXiv:1904.07004 (2019).

Why this paper? Cited by Combining Principles of Dependent Type Theory, Computational Synthetic Cohomology Theory in Homotopy Type Theory, and Formalizing the ∞-Categorical Yoneda Lemma

A week chewed up by caring for family members with covid was not the week to dive too deeply into this paper, whose mathematics go well beyond what I have available at command, so I’ll keep this short and high level (aided, I must say, by this paper’s excellent introduction).

I have written before about 2-category theory, where we have objects, arrows between objects, and arrows (sometimes called 2-cells) between those arrows. The canonical example are collections of categories, which have layers of categories; functors; and natural transformations. ∞-categories generalise this to an infinite stack of layers of n-cells. An (∞,1)-category is a special case (see ncatlab on (n,r)-categories to explain the notation) in which every n-cell after level 1 is an equivalence. This puts us into the realm of homotopy theory, where we have paths, paths between paths, and so on ad infinitum. This paper looks at such categories which are additionally (higher) toposes.

The motivation for these structures proceeds by analogy with the mathematics of non-infinitary toposes. Toposes are of course categories and so we can work ‘arrow-theoretically’ with commuting diagrams, explicit reasoning about the uniqueness of certain arrows, and so forth, but this approach is, according to Shulman, “tedious and verbose”. Instead we often work ‘synthetically’ with intuitionistic (typed) higher order logic, as this logic can be interpreted in any topos. In this context, this logic is called the internal language of the topos(es). (∞,1)-categories enter the picture because they are intended to have a similar relationship with homotopy type theory.

For this story to work we need confidence that we can interpret homotopy type theory into any (∞,1)-category. This cannot work naively because of irritating coherence issues: constructions which are strict equalities in the type theory correspond only to equivalences in the category theory, and so it becomes impossible to unambiguously define *the* interpretation of these constructions. This is a standard problem in the denotational semantics of dependent type theory and is solved by showing all categories of interest can be ‘strictified’ into categories where everything that needs to be an equality is one. With (∞,1)-categories this proceeds by something called a (Quillen) model category. This paper fills in a major gap in this interpretation – and judging by its length and complexity, it is not easy work! – by showing that the crucial property of univalence, the main motivation for homotopy type theory in the first place, can be forced to hold in such strictified categories, via a new construction called a type-theoretic model topos.