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

https://arxiv.org/abs/1701.07538

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

We say that a type is small if it is in

**Theorem. ***Let be a type with , and let be a type with . Then the following are equivalent.*

*The total space*is contractible. *The canonical map*defined by path induction, mapping to , 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*. In other words, is in the connected component of the type family .

There are at least two equivalent ways of saying that a (possibly large) type

- For each
there is a type and an equivalence . - For each
there is a type ; for each there is a term , and the canonical dependent function defined by path induction by sending to 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

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

**Main Theorem.** *Let be a univalent universe that is closed under pushouts. Suppose that , that is a locally small type, and let . Then we can construct*

*a small type*, *a factorization**such that*is an embedding that satisfies the universal property of the image inclusion, namely that for any embedding , of which the domain is possibly large, if factors through , then so does .

Recall that

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

In the case

Below, I will indicate how we can use the above theorem to construct the n-truncations for any

**Theorem.*** Let be a univalent universe that is closed under pushouts. Then we can define for any *

*an n-truncation operation*, *a map**such that for any*, the type is n-truncated and satisfies the (dependent) universal property of n-truncation, namely that for every type family of possibly large types such that each is n-truncated, the canonical map

given by precomposition byis an equivalence.

*Construction.* The proof is by induction on

First, we define

For the proof that