Constructing the Propositional Truncation using Nonrecursive HITs

In this post, I want to talk about a construction of the propositional truncation of an arbitrary type using only non-recursive HITs. The whole construction is formalized in the new proof assistant Lean, and available on Github. I’ll write another blog post explaining more about Lean in August.

The construction of the propositional truncation of a type $A$ is as follows. Let $\{A\}$ be the following HIT:

HIT {-} (A : Type) : Type :=

| f : A → {A}

| e : ∀(a b : A), f a = f b

I call this the “one step truncation”, because the HIT is like the propositional truncation, but takes out the recursive part. Martin Escardo calls this the generalized circle, since $\{\mathbf{1}\} \simeq S^1$ . We can repeat this multiple times: $A_0 :\equiv A$ and $A_{n+1} :\equiv \{A_n\}$ . Now the colimit $A_\infty$ of this sequence is the propositional truncation of $A$ : $A_\infty \simeq \| A \|$ . To make sure we’re on the same page, and to introduce the notation I use for the constructors, the (sequential) colimit is the following HIT: (I will mostly leave the arguments in $\mathbb{N}$ implicit)

HIT colimit (A : ℕ → Type)

(f : ∀(n : ℕ), A n → A (n+1)) : Type :=

| i : ∀(n : ℕ), A n → colimit A f

| g : ∀(n : ℕ) (a : A n), i (f a) = i a

Below I’ll give an intuition of why the construction works, and after that a proof. But first I want to talk about some consequences of the construction.

First of all this is the first instance of a HIT which has a recursive path constructor which has been reduced to non-recursive HITs. During the HoTT workshop in Warsaw there was a conjecture that all HITs with recursive (higher) path constructors can be reduced to HITs where only point constructors are allowed to be recursive. Although I have no idea whether this conjecture is true in general, this is the first step towards proving it.

Secondly, this gives an alternative answer to the question about the universal property of the propositional truncation. This construction shows that (using function extensionality) a function $h : \|A\| \to B$ for an arbitrary type $B$ is “the same” as a sequence of functions $h_n : A_n \to B$ (with $A_n$ defined above) such that for all $a : A_n$ we have $h_{n+1}\ (f\ a) = h\ a$ . In a formula

$(\|A\| \to B)\ \simeq\ (\Sigma(h : \Pi n, A_n \to B), \Pi (n : \mathbb{N}) (a : A_n), h_{n+1}\ (f\ a) = h_n\ a)$ .

So, why does the construction work?
To give an intuition why this works consider the propositional truncation of the booleans, $\|2\|$ . Of course, this type is equivalent to the interval (and any other contractible type), but there is actually a little more going on. The path constructor of the propositional truncation (let’s call it $e'$ here) gives rise to two paths between $0_2$ and $1_{2}$ : $e'\ |0_{2}|\ |1_{2}|$ and $(e'\ |1_{2}|\ |0_{2}|)^{-1}$ . Since the resulting type is a mere proposition, these paths must be equal. We can construct a path between them explicitly by using the continuity of $e'$ . We can prove that for every $x : \|2\|$ and every $p : |0_2| = x$ we have $p = (e' \ |0_{2}|\ |0_{2}|)^{-1}\cdot e' \ |0_{2}|\ x$ by path induction, and this leads to the conclusion that any two elements in $|0_2| = |1_{2}|$ are equal. This is exactly the proof that any proposition is a set.

Now consider the type $\{2\}$ . This is a type with points $a:\equiv f\ 0_2$ and $b:\equiv f\ 1_2$ and we have two paths from $a$ to $b$ . Let’s call them $p:\equiv e\ 0_2\ 1_2$ and $q:\equiv(e\ 1_2\ 0_2)^{-1}$ . These two paths are not equal. Of course, we also have a loop at both $a$ and $b$ .
However, in the type $\{\{2\}\}$ the corresponding paths $\text{ap}_f\ p$ and $\text{ap}_f\ q$ of type $f\ a = f\ b$ are equal. To see this, we can mimic the above proof. We can prove that for all $x : \{2\}$ and all $p : a = x$ we have $\text{ap}_f\ p = (e\ a\ a)^{-1} \cdot e\ a\ x$ , just by path induction on $p$ . Then we can conclude that $\text{ap}_f\ p = \text{ap}_f\ q$ . Of course, in $\{\{2\}\}$ there are new paths of type $f\ a = f\ b$ , but they will be identified again in $\{\{\{2\}\}\}$ .

<sidenote>
The above argument also shows that if any function $f$ is weakly constant, then $\text{ap}_f : x = y \to f\ x = f\ y$ is weakly constant for any $x,y$ (using the terminology of this post).
</sidenote>

So this is the intuition why $A_\infty$ is the propositional truncation of $A$ . In $\{A\}$ a path is added between any two points of $A$ , between any two existing parallel paths (and between any two parallel higher paths). Then in $\{\{A\}\}$ higher paths are added between all newly introduced (higher) paths, and so on. In the colimit, paths exist between any two points, parallel paths, and parallel higher paths, so we get the propositional truncation.

The proof.
But this is just the intuition. How do we prove that we get the propositional truncation? We clearly get the point constructor for the propositional truncation, because $i_0$ (the constructor of the colimit) has type $A \to A_\infty$ . Now we still have to show two things:

We have to show that $A_\infty$ is a mere proposition
We have to construct the induction principle for the propositional truncation on $A_\infty$ , with the judgmental computation rule

2. The second part is easy. If we’re given a family of propositions $P : A_\infty \to \text{Prop}$ with a map $h : \Pi(a : A), P\ (i_0\ a)$ we have to construct a map $k : \Pi(x : A_\infty), P\ x$ . We do this by induction on $x : A_\infty$ . Since we construct something in $P\ a$ , which is a mere proposition, the path construction is automatic, and we only have to deal with the case that $x\equiv i_n\ a$ for some $n : \mathbb{N}$ and $a : A\ n$ . Now we do induction on $n$ .
If $n\equiv0$ , we can choose the element $h\ a : P\ (i_0\ a)$ .
If $n\equiv k+1$ , we know that $a : \{A_k\}$ , so we can induct on $a$ . If $a\equiv f\ b$ , we need an element of $P\ (i_{n+1}\ (f\ b))$ . We have an element of $P\ (i_n\ b)$ by induction hypothesis. So we can transport this point along the equality $(g_n\ b)^{-1} : i_n\ b = i_{n+1}\ (f\ b)$ to get the desired point. The path construction is again automatic. In pattern matching notation we have defined:

$k\ (i_{0}\ a) :\equiv h\ a$ and
$k\ (i_{n+1}\ (f\ b)) :\equiv (g_n\ b)^{-1}_*(k\ (i_n\ b))$ .

The definition $k\ (i_{0}\ a) :\equiv h\ a$ is also the (judgmental) computation rule for the propositional truncation.

1. So we only need to show that $A_\infty$ is a mere proposition, i.e. $\Pi(x\ y : A_\infty), x = y$ . We first do induction on $x$ . Note that $\Pi(y : A _\infty), x = y$ is a mere proposition. (Left as exercise to the reader. Hint: assume that it is inhabited.) So we only have to consider the case where $x$ is a point constructor, say $x\equiv i_n\ a$ . Now we do induction on $y$ . Now the goal is $i_n\ a = y$ , and we don’t know (yet) that this is a mere proposition, so we have to show two things:

We have to construct a $p\ a\ b : i_n\ a = i_m\ b$ for all $n,m,a,b$ ;
We have to show that $p$ satisfies the following coherence condition: $p\ a\ (f\ b)\ \cdot\ g_m\ b = p\ a\ b$ .

In particular, we want to make the construction of $p$ as simple as possible, so that the coherence condition for $p$ remains doable.

For the construction of $p$ , let’s first consider a special case where $a$ and $b$ live in the same level, i.e. where $n \equiv m$ . This will be used in the general construction. In this case, we have $i_n\ a = i_{n+1}\ (f\ a) = i_{n+1}\ (f\ b) = i_n\ b$ , where the second equality is by the path constructor $e$ of $\{A_n\}$ and the other two equalities are by the path constructor $g$ of the colimit. Let’s call this equality $q\ a\ b : i_n\ a = i_n\ b$ .

For the general construction of $p$ with arbitrary $n$ and $m$ , I have considered three approaches. I will first discuss two approaches where I failed to complete the proof.

(failed) Approach 1. Induct on both $n$ and $m$ . In the successor case, induct on $a$ and $b$ . Unfortunately, this becomes horrible very quickly, because we now have a nested double induction on HITs. This means that we already need to prove coherence conditions just to construct $p$ , and after that we still need to show that $p$ satisfies a coherence condition. I quickly gave up on this idea.

(failed) Approach 2. Lift $a$ and $b$ both to $A\ (n + m)$ by repeatedly applying $f$ , and then show that $i_n\ a = i_{n+m}\ (f^m\ a) = i_{n+m}\ (f^n\ b) = i_m\ b$ , where the second equality is $q\ (f^m\ a)\ (f^n\ b)$ . This works, but there is a catch: $f^m\ a$ lives in $A (n + m)$ and $f^n\ b$ lives in $A (m + n)$ (assuming addition is defined by induction on the second argument). So to complete the construction, we also have to transport along the equality $n+m=m+n$ . This is fine, but for the coherence condition for $p$ this transport becomes an annoying obstacle. Showing the coherence condition is possible, but I didn’t see how to do it. Then realized there was a more convenient approach, where I didn’t have to worry about transports.

(succeeded) Approach 3. Distinguish cases between $n\le m$ and $m \le n$ and induct on those inequalities. I’m assuming that the inequality is defined by an (ordinary) inductive family

inductive le (n : ℕ) : ℕ → Type :=

| refl : le n n

| step : Π(m : ℕ), le n m → le n (m+1)

This definition gives a very useful induction principle for this construction. If $H : m\le n$ we can construct a map $f^H : A\ m \to A\ n$ by induction on $H$ :

$f^{\text{refl}_n}\ a:\equiv a$ ;
$f^{\text{step}\ H}\ a:\equiv f\ (f^H\ a)$ .

I use the notation $f^H$ for this, similar to $f^n$ , because we repeatedly apply $f$ and the number of times is determined by $H$ . Since the type $m \le n$ is a mere proposition, $f^H$ doesn’t really depend on $H$ , only on the fact that its type $m \le n$ has an inhabitant.
We can now also show that $g^H\ b : i_n\ (f^H\ b) = i_m\ b$ by induction on $H$ as concatenation of multiple $g$ s. Now if $H : m \le n$ we can construct $p\ a\ b$ by $i_n\ a = i_n\ (f^H\ b) = i_m\ b$ , where the first equality is $q\ a\ (f^H\ b)$ . The case $n \le m$ is similar.

This is a nice and simple construction of $p$ (without transports), and we can prove the coherence conditions using this definition, but that is more involved.

We have constructed $p$ in such a way that for $H : n \le m$ we have that $p\ a\ b$ equals $(g^H\ a)^{-1}\ \cdot\ q\ (f^H\ a)\ b$ and in the case that $H : m \le n$ we have that $p\ a\ b$ equals $q\ a\ (f^H\ b)\ \cdot\ g^H\ b$ . This is not purely by definition, for the case $n = m$ we have to prove something here, because we cannot get both inequalities by definition.

Now we have to show that $p\ a\ (f\ b)\ \cdot\ g_m\ b = p\ a\ b$ . We distinguish two cases: $n > m$ and $n \le m$ .

Case $n > m$
In this case we can find $H : m+1 \le n$ and $H' : m \le n$ . In this case $p\ a\ b = q\ a\ (f^{H'}\ b)\ \cdot\ g^H\ b$ and $p\ a\ (f\ b) = q\ a\ (f^{H}\ (f\ b))\ \cdot\ g^H\ (f\ b)$

The situation is displayed below (click image for larger view). Some arguments of paths are omitted, and the maps $i$ and $\text{ap}_i$ are also omitted for readability (the actual equalities live in $A_\infty$ ). We need to fill the pentagon formed by the outer (thick) equalities.

By induction on $H$ we can find a path $r : f^{H'}\ b = f^H\ (f\ b)$ and by another induction on $H$ we can fill the bottom square in the diagram. We will skip the details here. The top triangle can be filled for a general path $r$ by induction on $r$ . This finishes the case $n > m$ .

Case $n \le m$
Now we can find $H : n \le m$ and $H' : n \le m+1$ . Here $p\ a\ b = (g^H\ a)^{-1}\ \cdot\ q\ (f^H\ a)\ b$ and $p\ a\ (f\ b) = (g^{H'}\ a)^{-1}\ \cdot\ q\ (f^{H'}\ a)\ (f\ b)$ . The situation is below.

If we choose $H'$ correctly (namely as $\text{step}\ H$ ), then by definition $f^{H'}\ a\equiv f\ (f^H\ a)$ and $g^{H'}\ a\equiv g\ (f^H\ a)\ \cdot\ g^H\ a$ , so the triangle in the left of the diagram is a definitional equality. We can prove the remaining square in more generality. See the below diagram, where we mention $i$ explicitly.

The bottom square is filled by induction on $p$ . To show that the two paths in the top are equal, first note that $i_{k+1} : A_{k+1} \to A_\infty$ is weakly constant, because that is exactly the type of $q$ . So $\text{ap}_i : f\ x = f\ y \to i\ (f\ x) = i\ (f\ y)$ is weakly constant. This finishes the case $n \le m$ , and hence the proof that $A_\infty$ is a mere proposition.

Future Work
The natural question is whether we can construct arbitrary $n$ -truncations using non-recursive HITs. The construction in this post can be easily generalized by using an “one-step $n$ -truncation,” but the proof that the resulting type is $n$ -truncated cannot be generalized easily. However, Egbert Rijke has a proof sketch of the construction of localizations between $\omega$ -compact types using nonrecursive HITs, and these include all the $n$ -truncations.

Constructing the Propositional Truncation using Nonrecursive HITs

Constructing the Propositional Truncation using Nonrecursive HITs

Recommend

A new class of models for the univalence axiom

Real-cohesive homotopy type theory

Combinatorial Species and Finite Sets in HoTT

HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics

Parametricity, automorphisms of the universe, and excluded middle

Type theoretic replacement & the n-truncation

A hands-on introduction to cubicaltt

In memoriam: Vladimir Voevodsky

Impredicative Encodings of Inductive Types in HoTT

A self-contained, brief and complete formulation of Voevodsky’s univalence axiom

About Joyk