The join construction

TL;DR

This paper introduces a join construction in homotopy type theory, establishing its algebraic properties, connectivity behavior, and applications to defining images, quotients, and truncations within univalent foundations.

Contribution

It develops a join operation with key properties, proves the join connectivity theorem, and applies the construction to define images, set-quotients, Rezk completion, and truncations in homotopy type theory.

Findings

The join operation is commutative, associative, and has a neutral element.

The join connectivity theorem relates the connectivity of joins to individual maps.

Applications include constructing images, quotients, and truncations within the type-theoretic framework.

Abstract

In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from the empty type into the common codomain is a neutral element. Moreover, we show that the idempotents of the join of maps are precisely the embeddings, and we prove the `join connectivity theorem', which states that the connectivity of the join of maps equals the join of the connectivities of the individual maps. We define the image of a map $f:A\to X$ in $U$ via the join construction, as the colimit of the finite join powers of $f$. The join powers therefore provide approximations of the image inclusion, and the join connectivity theorem implies that the approximating maps into the image increase in connectivity. A modified version of the join construction can be used to show that for any map $f:A\to X$ in which $X$ is only assumed to be locally small, the image is a small type. We use the modified join construction to give an alternative construction of set-quotients, the Rezk completion of a precategory, and we define the $n$-truncation for any $n:\mathbb{N}$. Thus we see that each of these are definable operations on a univalent universe for Martin-L\"of type theory with a natural numbers object, that is moreover closed under homotopy coequalizers.