Discrete homotopy hypothesis for n-types

TL;DR

This paper establishes an equivalence between discrete and classical homotopy theories at a fixed level n, providing explicit computations of discrete homotopy groups for complex structures.

Contribution

It introduces an explicit inverse to the graph nerve functor for n-fibrant cubical sets, bridging discrete and classical homotopy theories and enabling new computations.

Findings

Discrete and classical homotopy theories are equivalent after localization at n-equivalences.

Constructed an explicit homotopy inverse to the graph nerve functor.

Computed new discrete homotopy groups of cube boundaries and suspensions.

Abstract

We show that discrete and classical homotopy theories are equivalent after localizing at n-equivalences for any non-negative integer n. By constructing an explicit homotopy inverse to the graph nerve functor associating an n-fibrant cubical set to a graph, we are also able to give explicit computations of several previously unknown discrete homotopy groups of boundaries of cubes and suspensions of cycles.