The join construction

MaRDI QIDQ6282427zbMATH OpenFDO

Authors Egbert Rijke

Publication date 25 January 2017

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:AoX$ 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:AoX$ 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:mathbbN$. 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.

This page was built for publication: The join construction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6282427)