Constructive homotopy theory of marked semisimplicial sets

TL;DR

This paper develops a constructive homotopy theory for semisimplicial sets and marked semisimplicial sets, providing models for $oldsymbol{ extomega}$-groupoids and $(oldsymbol{ extomega, 1})$-categories without relying on classical topology.

Contribution

It introduces a constructive framework for homotopy theory of semisimplicial sets and extends it to marked semisimplicial sets, offering new proofs and models for higher categories.

Findings

Unit of free simplicial set adjunction is a weak equivalence

Geometric and cartesian products of fibrant semisimplicial sets are weakly equivalent

Constructive models for $oldsymbol{ extomega}$-groupoids and $(oldsymbol{ extomega, 1})$-categories

Abstract

We develop the homotopy theory of semisimplicial sets constructively and without reference to point-set topology to obtain a constructive model for $\omega$-groupoids. Most of the development is folklore, but for a few results the author is unaware of previously known constructive proofs. These include the statements that the unit of the free simplicial set adjunction is valued in weak equivalences and that the geometric product and cartesian product of fibrant semisimplicial sets are weakly equivalent. We then extend the development to marked semisimplicial sets in order to obtain a constructive model for $(\omega, 1)$-categories.