Type theoretic replacement & the n-truncation

This post is to announce a new article that I recently uploaded to the arxiv:

The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in set theory, the replacement axiom asserts that if $F$ is a class function, assigning to any set $X$ a new set $F(X)$ , then the image of any set $A$ , i.e. the set $\{F(X)\mid X\in A\}$ is again a set. In homotopy type theory we consider instead a map $f : A\to X$ from a small type $A:U$ into a locally small type $X$ , and our main result is the construction of a small type $\mathrm{im}(f)$ with the universal property of the image of $f$ .

We say that a type is small if it is in $U$ , and for the purpose of this blog post smallness and locally smallness will always be with respect to $U$ . Before we define local smallness, let us recall the following rephrasing of the `encode-decode method’, which we might also call the Licata-Shulman theorem:

Theorem. Let $A$ be a type with $a:A$ , and let $P: A\to U$ be a type with $p:P(a)$ . Then the following are equivalent.

The total space $\Sigma_{(b:A)} P(b)$ is contractible.
The canonical map $\Pi_{(b:A)} (a=b)\to P(b)$ defined by path induction, mapping $\mathrm{refl}_a$ to $p$ , is a fiberwise equivalence.

Note that this theorem follows from the fact that a fiberwise map is a fiberwise equivalence if and only if it induces an equivalence on total spaces. Since for path spaces the total space will be contractible, we observe that any fiberwise equivalence establishes contractibility of the total space, i.e. we might add the following equivalent statement to the theorem.

There (merely) exists a family of equivalences $e:\Pi_{(b:B)} (a=b)\simeq P(b)$ . In other words, $P$ is in the connected component of the type family $b\mapsto (a=b)$ .

There are at least two equivalent ways of saying that a (possibly large) type $X$ is locally small:

For each $x,y:X$ there is a type $(x='y):U$ and an equivalence $e_{x,y}:(x=y)\simeq (x='y)$ .
For each $x,y:X$ there is a type $(x='y):U$ ; for each $x:X$ there is a term $r_X:x='x$ , and the canonical dependent function $\Pi_{(y:X)} (x=y)\to (x='y)$ defined by path induction by sending $\mathrm{refl}_x$ to $r_x$ is an equivalence.

Note that the data in the first structure is clearly a (large) mere proposition, because there can be at most one such a type family $(x='y)$ , while the equivalences in the second structure are canonical with respect to the choice of reflexivity $r_x$ . To see that these are indeed equivalent, note that the family of equivalences in the first structure is a fiberwise equivalence, hence it induces an equivalence on total spaces. Therefore it follows that the total space $\Sigma_{(y:X)} (x='y)$ is contractible. Thus we see by Licata’s theorem that the canoncial fiberwise map is a fiberwise equivalence. Furthermore, it is not hard to see that the family of equivalences $e_{x,y}$ is equal to the canonical family of equivalences. There is slightly more to show, but let us keep up the pace and go on.

Examples of locally small types include any small type, any mere proposition regardless of their size, the universe is locally small by the univalence axiom, and if $A$ is small and $X$ is locally small then the type $A\to X$ is locally small. Observe also that the univalence axiom follows if we assume the `uncanonical univalence axiom’, namely that there merely exists a family of equivalences $e_{A,B} : (A=B)\simeq (A\simeq B)$ . Thus we see that the slogan ‘identity of the universe is equivalent to equivalence’ actually implies univalence.

Main Theorem. Let $U$ be a univalent universe that is closed under pushouts. Suppose that $A:U$ , that $X$ is a locally small type, and let $f:A\to X$ . Then we can construct

a small type $\mathrm{im}(f):U$ ,
a factorization
such that $i_f$ is an embedding that satisfies the universal property of the image inclusion, namely that for any embedding $g$ , of which the domain is possibly large, if $f$ factors through $g$ , then so does $i_f$ .

Recall that $f$ factors through an embedding $g$ in at most one way. Writing $\mathrm{Hom}_X(f,g)$ for the mere proposition that $f$ factors through $g$ , we see that $i_f$ satisfies the universal property of the image inclusion precisely when the canonical map

$\mathrm{Hom}_X(i_f,g)\to\mathrm{Hom}_X(f,g)$

is an equivalence.

Most of the paper is concerned with the construction with which we prove this theorem: the join construction. By repeatedly joining a map with itself, one eventually arrives at an embedding. The join of two maps $f:A\to X$ and $g:B\to X$ is defined by first pulling back, and then taking the pushout, as indicated in the following diagram

join_maps

In the case $X \equiv \mathbf{1}$ , the type $A \ast_X B$ is equivalent to the usual join of types $A \ast B$ . Just like the join of types, the join of maps with a common codomain is associative, commutative, and it has a unit: the unique map from the empty type into $X$ . The join of two embeddings is again an embedding. We show that the last statement can be strengthened: the maps $f:A\to X$ that are idempotent in a canonical way (i.e. the canonical morphism $f \to f \ast f$ in the slice category over $X$ is an equivalence) are precisely the embeddings.

Below, I will indicate how we can use the above theorem to construct the n-truncations for any $n\geq -2$ on any univalent universe that is closed under pushouts. Other applications include the construction of set-quotients and of Rezk-completion, since these are both constructed as the image of the Yoneda-embedding, and it also follows that the univalent completion of any dependent type $P:A\to U$ can be constructed as a type in $U$ , namely $\mathrm{im}(P)$ , without needing to resort to more exotic higher inductive types. In particular, any connected component of the universe is equivalent to a small type.

Theorem. Let $U$ be a univalent universe that is closed under pushouts. Then we can define for any $n\geq -2$

an n-truncation operation $\|{-}\|_n:U\to U$ ,
a map $|{-}|:\Pi_{(A:U)} A\to \|A\|_n$
such that for any $A:U$ , the type $\|A\|_n$ is n-truncated and satisfies the (dependent) universal property of n-truncation, namely that for every type family $P:\|A\|_n\to\mathrm{Type}$ of possibly large types such that each $P(x)$ is n-truncated, the canonical map
$(\Pi_{(x:\|A\|_n)} P(x))\to (\Pi_{(a:A)} P(|a|_n))$
given by precomposition by $|{-}|_n$ is an equivalence.

Construction. The proof is by induction on $n\geq -2$ . The case $n\equiv -2$ is trivial (take $A\mapsto \mathbf{1}$ ). For the induction hypothesis we assume an n-truncation operation with structure described in the statement of the theorem.

First, we define $\mathcal{Y}_n:A\to (A\to U)$ by $\mathcal{Y}_n(a,b):\equiv \|a=b\|_n$ . As we have seen, the universe is locally small, and therefore the type $A\to U$ is locally small. Therefore we can define