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 is a class function, assigning to any set a new set , then the image of any set , i.e. the set is again a set. In homotopy type theory we consider instead a map from a small type into a locally small type , and our main result is the construction of a small type with the universal property of the image of .
We say that a type is small if it is in , and for the purpose of this blog post smallness and locally smallness will always be with respect to . 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 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 is locally small:
- 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 , while the equivalences in the second structure are canonical with respect to the choice of reflexivity . 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 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 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 is small and is locally small then the type 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 . Thus we see that the slogan ‘identity of the universe is equivalent to equivalence’ actually implies univalence.
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 factors through an embedding in at most one way. Writing for the mere proposition that factors through , we see that satisfies the universal property of the image inclusion precisely when the canonical map
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 and is defined by first pulling back, and then taking the pushout, as indicated in the following diagram
In the case , the type is equivalent to the usual join of types . 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 . The join of two embeddings is again an embedding. We show that the last statement can be strengthened: the maps that are idempotent in a canonical way (i.e. the canonical morphism in the slice category over 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 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 can be constructed as a type in , namely , 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 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 by is an equivalence.
Construction. The proof is by induction on . The case is trivial (take ). For the induction hypothesis we assume an n-truncation operation with structure described in the statement of the theorem.
First, we define by . As we have seen, the universe is locally small, and therefore the type is locally small. Therefore we can define
For the proof that is indeed -truncated, and satisfies the universal property of the n-truncation we refer to the article.