An Elementary Approach to Truncations

TL;DR

This paper presents an elementary, universe-based approach to defining and analyzing truncations and localizations in higher category theory, enabling classical results and new insights in non-presentable contexts.

Contribution

It introduces an elementary method for truncations and localizations using universes, providing new tools for studying $( abla, 1)$-categories and toposes.

Findings

Elementary construction of truncation functors

Proof of Blakers-Massey theorem in elementary setting

Application to non-presentable $( abla, 1)$-categories

Abstract

We study truncated objects using elementary methods. Concretely, we use universes and the resulting natural number object to define internal truncation levels and prove they behave similar to standard truncated objects. Moreover, we take an elementary approach to localizations, giving various equivalent conditions that characterize localizations and constructing a localization out of a sub-universe of local objects via an internal right Kan extension. We then use this general approach, as well as an inductive approach, to construct truncation functors. We use the resulting truncation functors to prove classical results about truncations, such as Blakers-Massey theorem, in the elementary setting. We also give examples of non-presentable $(\infty, 1)$-categories where the elementary approach can be used to define and compute truncations. Finally, we turn around and use truncations to study elementary $(\infty, 1)$-toposes and show how they can help us better understand subobject classifiers and universes