Presentation of finite Reedy categories as localizations of finite direct categories

In this paper, we present a construction from a Reedy category $C$ of a direct category $\mathrm{Down}(C)$ and a functor $\mathrm{Down}(C)\to C$, which exhibits $C$ as an $(\mathrm{\infty },1)$-categorical localization of $\mathrm{Down}(C)$. This result refines previous constructions in the literature by ensuring finiteness of the direct category $\mathrm{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.