Related papers: Filter Quotients and Non-Presentable $(\infty,1)$-…

The filter quotient construction is a particular instance of a filtered colimit of categories. It has primarily been considered in the context of categorical logic, where it has been used effectively to construct non-trivial models, for…

Homotopy type theory is a modern foundation for mathematics that introduces the univalence axiom and is particularly suitable for the study of homotopical mathematics and its formalization via proof assistants. In order to better comprehend…

We define an elementary $\infty$-topos that simultaneously generalizes an elementary topos and Grothendieck $\infty$-topos. We then prove it satisfies the expected topos theoretic properties, such as descent, local Cartesian closure,…

While many different models for $(\infty,1)$-categories are currently being used, it is known that they are Quillen equivalent to one another. Several higher-order analogues of them are being developed as models for $(\infty,…

We introduce a notion of a filtered model structure and use this notion to produce various model structures on pro-categories. This framework generalizes several known examples. We give several examples, including a homotopy theory for…

We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language…

We prove a single category-theoretic result encapsulating the notions of ultrafilters, ultrapower, ultraproduct, tensor product of ultrafilters, the Rudin--Kiesler partial ordering on ultrafilters, and Blass's category of ultrafilters UF.…

We propose a definition of higher inductive types in $(\infty,1)$-categories with finite limits. We show that the $(\infty,1)$-category of $(\infty,1)$-categories with higher inductive types is finitarily presentable. In particular, the…

This note recalls the representation of regular theories T in terms of set-valued functors on models given by Makkai(1990), and explicitly states the representation theorem for the classifying topos Set[T] in terms of filtered colimit…

We study properties of a category after quotienting out a suitable chosen group of isomorphisms on each object. Coproducts in the original category are described in its quotient by our new weaker notion of a 'phased coproduct'. We examine…

We prove that every elementary $(\infty,1)$-topos has a natural number object. We achieve this by defining the loop space of the circle and showing that we can construct a natural number object out of it. Part of the proof involves showing…

We define a notion of "theory of (1,infty)-categories", and we prove that such a theory is unique up to equivalence.

We construct classifying $\infty$-topoi by showing that the $(\infty,2)$-category of topoi has weighted limits. We show that several prestacks of interest have a classifying topos, including the prestack of spectra.

We define the notion of 2-filtered 2-category and give an explicit construction of the bicolimit of a category valued 2-functor. A category considered as a trivial 2-category is 2-filtered if and only if it is a filtered category, and our…

We define a category of filtered topological spaces and explore some of its homotopy theoretic properties, including a filtered analogue of CW approximation. With this, we define and study a filtered (weighted) variant of the Euler…

Reasoning about weak higher categorical structures constitutes a challenging task, even to the experts. One principal reason is that the language of set theory is not invariant under the weaker notions of equivalence at play, such as…

Quillen defined a {\em model category} to be a category with finite limits and colimits carrying a certain extra structure. In this paper, we show that only finite products and coproducts (in addition to the certain extra structure alluded…

We define a functor which takes in an $(\infty,1)$-category and outputs an $(\omega,1)$-category, the natural maximally "strict" version of an $(\infty,1)$-category. We do this by modeling $(\infty,1)$-categories as categories enriched in…

We show how to treat families of $\infty$-categories fibered in categorical patterns (e.g., $\infty$-operads and monoidal $\infty$-categories) in terms of fibrations by relativizing the Grothendieck construction. As applications, we…

Riehl and Verity have established that for a quasi-category $A$ that admits limits, and a homotopy coherent monad on $A$ which does not preserve limits, the Eilenberg-Moore object still admits limits; this can be interpreted as a…