Presentation of finite Reedy categories as localizations of finite direct categories

TL;DR

This paper constructs a finite direct category from a finite Reedy category, showing that the original category can be viewed as a localization of this simpler structure, with potential applications in homotopy type theory.

Contribution

It refines existing methods by ensuring the finiteness of the direct category, enabling applications in finitely truncated simplicial types within homotopy type theory.

Findings

Constructs a finite direct category from a finite Reedy category.

Shows the original Reedy category as a localization of the constructed category.

Potential application to meta-theory of finitely truncated simplicial types.

Abstract

In this paper, we present a construction from a Reedy category $C$ of a direct category $\operatorname{Down}(C)$ and a functor $\operatorname{Down}(C) \to C$, which exhibits $C$ as an $(\infty,1)$-categorical localization of $\operatorname{Down}(C)$. This result refines previous constructions in the literature by ensuring finiteness of the direct category $\operatorname{Down}(C)$ whenever $C$ is finite, which is not guaranteed by existing approaches. The finiteness property is useful when we want to embed the construction into the syntax of a (non-infinitary) logic: the author expects the construction may be used to develop a meta-theory of finitely truncated simplicial types for homotopy type theory.