Universal Properties of Truncations

Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation $\Vert - \Vert$ , and I want to write this blog post in case someone could not attend the talk but is interested nevertheless. There are also my slides and the arXiv paper.
The topic of my talk can be summarised as

Question: What is the type $\Vert A \Vert \to B$ ?

This question is very easy if $B$ is propositional, because then we have

Partial answer (1): If $B$ is propositional, then $(\Vert A \Vert \to B) \simeq (A \to B)$

by the usual universal property, with the equivalence given by the canonical map. Without an assumption on $B$ , it is much harder.

The rest of this post contains a special case which already contains some of the important ideas. It is a bit lengthy, and in case you don’t have time to read everything, here is the

Main result (general universal property of the propositional truncation).
In a dependent type theory with at least $\mathbf{1}$ , $\Sigma$ -, $\Pi$ -, and identity types, which furthermore has Reedy $\omega^{\mathsf{op}}$ -limits (“infinite $\Sigma$ -types”), we can define the type of coherently constant functions $A \xrightarrow {\omega} B$ as the type of natural transformations between type-valued presheaves. If the type theory has propositional truncations, we can construct a canonical map from $\Vert A \Vert \to B$ to $A \xrightarrow {\omega} B$ . If the type theory further has function extensionality, then this canonical map is an equivalence.
If $B$ is known to be $n$ -truncated for some fixed $n$ , we can drop the assumption of Reedy $\omega^{\mathsf{op}}$ -limits and perform the whole construction in “standard syntactical” HoTT. This describes how functions $\Vert A \Vert \to B$ can be defined if $B$ is not known to be propositional, and it streamlines the usual approach of finding a propositional $Q$ with $A \to Q$ and $Q \to B$ .

Here comes the long version of this blog post. So, what is a function $g : \Vert A \Vert \to B$ ? If we think of elements of $\Vert A \Vert$ as anonymous inhabitants of $A$ , we could expect that such a $g$ is “the same” as a function $f : A \to B$ which “cannot look at its input”. But then, how can we specify what it means to “not look at its input” internally? A first attempt could be requesting that $f$ is weakly constant, $\mathsf{wconst}_f :\equiv \Pi_{x,y:A} f(x) = f(y)$ . Indeed, it has been shown:

Partial answer (2): If $B$ is a set (h-set, $0$ -truncated), then $(\Vert A \Vert \to B) \simeq (\Sigma (f : A \to B). \mathsf{wconst}_f)$ , where the function from left to right is the canonical one.

It is not surprising that we still need this strong condition on $B$ if we want weak constancy to be a sufficient answer: just throwing in a bunch of paths, which might or might not “fit together” (we just don’t know anything) seems wrong. Indeed, from Mike’s recent construction, we know that the statement does become false (contradicts univalence) without this requirement.

Given a function $f : A \to B$ and a proof $c : \mathsf{wconst}_f$ , we can try to fix the problem that the paths given by $c$ “do not fit together” by throwing in a coherence proof, i.e. an element of $\mathsf{coh}_{f,c} :\equiv \Pi_{x,y,z:A} c(x,y) \cdot c(y,z) = c(x,z)$ . We should already know that this will introduce its own problems and thus not fix everything, but at least, we get:

Partial answer (3): If $B$ is $1$ -truncated, then $(\Vert A \Vert \to B) \simeq (\Sigma (f : A \to B). \Sigma (c:\mathsf{wconst}_f). \mathsf{coh}_{f,c})$ , again given by a canonical map from left to right.

In my talk, I have given a proof of “partial answer (3)” via “reasoning with equivalences” (slides p. 5 ff). I start by assuming a point $a_0 : A$ . The type $B$ is then equivalent to the following (explanation below):

$\Sigma (f_1 : B).$
$\Sigma (f : A \to B). \Sigma (c_1 : \Pi_{a:A} f(a) = f_1).$
$\Sigma (c : \mathsf{const}_f). \Sigma(d_1 : \Pi_{a^1, a^2:A} c(a^1,a^2) \cdot c_1(a^2) = c_1(a^1)$
$\Sigma (c_2 : f(a_0) = f_1). \Sigma (d_3 : c(a_0,a_0) \cdot c_1(a_0) = c_2).$
$\Sigma (d : \mathsf{coh}_{f,c_0}).$
$\Sigma (d_2 : \Pi_{a:A} c(a_0,a) \cdot c_1(a) = c_2).$
$\mathbf{1}$

In the above long nested $\Sigma$ -type, the first line is just the $B$ that we start with. The second line adds two factors/ $\Sigma$ -components which, by function extensionality, cancel each other out (they form a singleton). The same is true for the pair in the third line, and for the pair in the fourth line. Lines five and six look different, but they are not really; it’s just that their “partners” (which would complete them to singletons) are hard to write down and, at the same time, contractible; thus, they are omitted. As $B$ is assumed to be a $1$ -type, it is easy to see that the $\Sigma$ -components in lines five and six are both propositional, and it’s also easy to see that the other $\Sigma$ -components imply that they are both inhabited. Of course, the seventh line does nothing.

Simply by re-ordering the $\Sigma$ -components in the above type, and not doing anything else, we get:

$\Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \Sigma(d : \mathsf{coh}_{f,c}).$
$\Sigma (f_1 : B) \Sigma(c_2 : f(a_0) = f_1).$
$\Sigma (c_1 : \Pi_{a:A} f(a) = f_1). \Sigma(d_2 : \Pi_{a:A} c(a_0,a) \cdot c_1(a) = c_2).$
$\Sigma (d_1 : \Pi_{a^1, a^2:A} c(a^1,a^2) \cdot c_1(a^2) = c_1(a^1)).$
$\Sigma (d_3 : c(a_0,a_0) \cdot c_1(a_0) = c_2).$
$\mathbf{1}$

By the same argument as before, the components in the pair in line two cancel each other out (i.e. the pair is contractible). The same is true for line three. Line four and five are propositional as $B$ is $1$ -truncated, but easily seen to be inhabited. Thus, the whole nested $\Sigma$ -type is equivalent to $\Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \mathsf{coh}_{f,c}$ .
In summary, we have constructed an equivalence $B \simeq \Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \mathsf{coh}_{f,c}$ . By going through the construction step-by-step, we see that the function part of the equivalence (map from left to right) is the canonical one (let’s write $\mathsf{canon}_1$ ), mapping $b : B$ to the triple $(\lambda \_. b, \lambda \_ \_ . \mathsf{refl}_b , \lambda \_ \_ \_ . \mathsf{refl}_{\mathsf{refl}_b})$ . Before we have started the construction, we have assumed a point $a_0 : A$ . But, and this is the crucial observation, the function $\mathsf{canon}_1$ does not depend on $a_0$ ! So, if the assumption $A$ implies that $\mathsf{canon}_1$ is an equivalence, then $\Vert A \Vert$ is already enough. Thus, we have $\Vert A \Vert \to \big(B \simeq \Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \mathsf{coh}_{f,c}\big)$ . We can move the $\Vert A \Vert \to$ -part to both sides of the equivalence, and on the right-hand side, we can apply the usual “distributivity of $\Sigma$ and $\Pi$ (or $\to$ )”, to move the $\Vert A \Vert \to$ into each $\Sigma$ -component; but in each $\Sigma$ -component, the $\Vert A \Vert$ gets eaten by an $A$ (we have that $\Vert A \Vert \to \Pi_{a : A}\ldots$ and $\Pi_{a:A} \ldots$ are equivalent), which gives us the claimed result.

The strategy we have used is very minimalistic. It does not need any “technology”: we just add and remove contractible pairs. For this “expanding and contracting” strategy, we have really only used very basic components of type theory ( $\Sigma$ , $\Pi$ , identity types with function extensionality, propositional truncation, but even that only in the very end). If we want to weaken the requirement on $B$ by one more level (i.e. if we want to derive a “universal property” which characterises $\Vert A \Vert \to B$ if $B$ is $2$ -truncated), we have to add one more coherence condition (which ensures that the $\mathsf{coh}_{f,c}$ -component is well-behaved). The core idea is that this expanding and contracting strategy can be done for any truncation level of $B$ , even if $B$ is not known to be $n$ -truncated at all, where the tower of conditions becomes infinite. I call an element of this “infinite $\Sigma$ -type” a coherently constant function from $A$ to $B$ .

The idea is that the $\Sigma$ -components $(f : A \to B)$ and $(c : \mathsf{const}_f)$ and $(d : \mathsf{coh}_{f,c})$ we used in the special case can be seen as components of a natural transformation between $[2]$ -truncated semi-simplicial types. By semi-simplicial type, I mean a Reedy fibrant diagram $\Delta_+^{\mathsf{op}} \to \mathcal{C}$ . By $[2]$ -truncated semi-simplicial types, I mean the “initial segments” of semi-simplicial types, the first three components $X_0, X_1, X_2$ as described here.
The first diagram we need is what I call the “trivial semi-simplicial type” over $A$ , written $T \! A$ , and its initial part is given by $T \! A_{[0]} :\equiv A$ , $T \! A_{[1]} :\equiv A \times A$ , and $T \! A_{[2]} :\equiv A \times A \times A$ . If we use the “fibred” notation (i.e. give the fibres over the matching objects), this would be $T \! A_{[0]} :\equiv A$ , $T \! A_{[1]}(a_1,a_2) :\equiv \mathbf{1}$ , $T \! A_{[2]}(a_1,a_2,a_3,\_,\_,\_) :\equiv \mathbf{1}$ . In the terminology of simplicial sets, this is the $[0]$ -coskeleton of [the diagram that is constantly] $A$ .
The second important diagram, I call it the equality semi-simplicial type over $B$ , is written $E \! B$ . One potential definition for the lowest levels would be given by (I only give the fibres this time): $E \! B_{[0]} :\equiv B$ , $E \! B_{[1]}(b_1,b_2) :\equiv b_1 = b_2$ , $E \! B_{[2]}(b_1,b_2,b_3,p_{12},p_{23},p_{13}) :\equiv p_{12} \cdot p_{23} = p_{13}$ . This is a fibrant replacement of $B$ . (We are lucky because $T \! A$ is already fibrant; otherwise, we should have constructed a fibrant replacement as well.)
If we now check what a (strict) natural transformation between $T \! A$ and $E \! B$ (viewed as diagrams over the full subcategory of $\Delta_+^{\mathsf{op}}$ with objects $[0],[1],[2]$ ) is, it is easy to see that the $[0]$ -component is exactly a map $f : A \to B$ , the $[1]$ -component is exactly a proof $c : \mathsf{const}_f$ , and the $[2]$ -component is just a proof $d : \mathsf{coh}_{f,c}$ . (The type of such natural transformations is given by the limit of the exponential of $T \! A$ and $E \! B$ .)

However, even with this idea, and with the above proof for the case that $B$ is $1$ -truncated, generalising this proof to the infinite case with infinitely many coherence conditions requires some ideas and a couple of technical steps which, for me, have been quite difficult. Therefore, it has taken me a very long time to write this up cleanly in an article. I am very grateful to the reviewers (this work is going to appear in the post-proceedings of TYPES’14) and to Steve (my thesis examiner) for many suggestions and interesting connections they have pointed out. In particular, one reviewer has remarked that the main result (the equivalence of coherently constant functions $A \xrightarrow{\omega} B$ and maps out of the truncation $\Vert A \Vert \to B$ ) is a type-theoretic version of Proposition 6.2.3.4 in Lurie’s Higher Topos Theory; and Vladimir has pointed out the connection to the work of his former student Alexander Vishik. Unfortunately, both are among the many things that I have yet to understand, but there is certainly a lot to explore. If you can see further connections which I have not mentioned here or in the paper, then this is very likely because I am not aware of them, and I’d be happy to hear about it!

3 Responses to Universal Properties of Truncations

Mike Shulman says:

20 July 2015 at 23:15

This is a very nice result! I really like how you use the category-theoretic point of view on type theories to give sense to “infinite contexts”.

Here’s a silly little question: can we generalize my counterexample from the other post to show that n-level coherence can’t be assumed to be sufficient in general if B is not n-truncated?

- Nicolai Kraus says:
  
  21 July 2015 at 12:28
  
  Thanks! I bet we can generalize your example, at least I would be very surprised if there was a fundamental problem which prevented us from doing that. At the moment, I don’t see how to do it though.
  
Pingback: Constructing the Propositional Truncation using Nonrecursive HITs | Homotopy Type Theory