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 is as follows. Let 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 . We can repeat this multiple times: and . Now the colimit of this sequence is the propositional truncation of : . 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 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 for an arbitrary type is “the same” as a sequence of functions (with defined above) such that for all we have . In a formula

.

**So, why does the construction work?**

To give an intuition why this works consider the propositional truncation of the booleans, . 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 here) gives rise to two paths between and : and . 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 . We can prove that for every and every we have by path induction, and this leads to the conclusion that any two elements in are equal. This is exactly the proof that any proposition is a set.

Now consider the type . This is a type with points and and we have two paths from to . Let’s call them and . These two paths are *not* equal. Of course, we also have a loop at both and .

However, in the type the corresponding paths and of type *are* equal. To see this, we can mimic the above proof. We can prove that for all and all we have , just by path induction on . Then we can conclude that . Of course, in there are *new* paths of type , but they will be identified again in .

<sidenote>

The above argument also shows that if any function is weakly constant, then is weakly constant for any (using the terminology of this post).

</sidenote>

So this is the intuition why is the propositional truncation of . In a path is added between any two points of , between any two *existing* parallel paths (and between any two parallel higher paths). Then in 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 (the constructor of the colimit) has type . Now we still have to show two things:

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

**2.** The second part is easy. If we’re given a family of propositions with a map we have to construct a map . We do this by induction on . Since we construct something in , which is a mere proposition, the path construction is automatic, and we only have to deal with the case that for some and . Now we do induction on .

If , we can choose the element .

If , we know that , so we can induct on . If , we need an element of . We have an element of by induction hypothesis. So we can transport this point along the equality to get the desired point. The path construction is again automatic. In pattern matching notation we have defined:

- and
- .

The definition is also the (judgmental) computation rule for the propositional truncation.

**1.** So we only need to show that is a mere proposition, i.e. . We first do induction on . Note that 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 is a point constructor, say . Now we do induction on . Now the goal is , and we don’t know (yet) that this is a mere proposition, so we have to show two things:

- We have to construct a for all ;
- We have to show that satisfies the following coherence condition: .

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

For the construction of , let’s first consider a special case where and live in the same level, i.e. where . This will be used in the general construction. In this case, we have , where the second equality is by the path constructor of and the other two equalities are by the path constructor of the colimit. Let’s call this equality .

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

(failed) **Approach 1.** Induct on both and . In the successor case, induct on and . 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 , and after that we still need to show that satisfies a coherence condition. I quickly gave up on this idea.

(failed) **Approach 2.** Lift and both to by repeatedly applying , and then show that , where the second equality is . This works, but there is a catch: lives in and lives in (assuming addition is defined by induction on the second argument). So to complete the construction, we also have to transport along the equality . This is fine, but for the coherence condition for 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 and 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 we can construct a map by induction on :

- ;
- .

I use the notation for this, similar to , because we repeatedly apply and the number of times is determined by . Since the type is a mere proposition, doesn’t really depend on , only on the fact that its type has an inhabitant.

We can now also show that by induction on as concatenation of multiple s. Now if we can construct by , where the first equality is . The case is similar.

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

We have constructed in such a way that for we have that equals and in the case that we have that equals . This is not purely by definition, for the case we have to prove something here, because we cannot get both inequalities by definition.

Now we have to show that . We distinguish two cases: and .

**Case **

In this case we can find and . In this case and

The situation is displayed below (click image for larger view). Some arguments of paths are omitted, and the maps and are also omitted for readability (the actual equalities live in ). We need to fill the pentagon formed by the outer (thick) equalities.

By induction on we can find a path and by another induction on 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 by induction on . This finishes the case .

**Case **

Now we can find and . Here and . The situation is below.

If we choose correctly (namely as ), then by definition and , 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 explicitly.

The bottom square is filled by induction on . To show that the two paths in the top are equal, first note that is weakly constant, because that is exactly the type of . So is weakly constant. This finishes the case , and hence the proof that is a mere proposition.

**Future Work**

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

This is very nice! In particular, it gives an answer to the following question: Suppose you want to eliminate using a function . What should the function satisfy? At least, it should be weakly constant. Your answer is that it is enough to exhibit a cocone whose first leg is the function . The second leg gives the weak constancy of . Then the other legs give the weak constancy of the previous legs. We may call such a function “coherently constant” if it can be completed to such a cocone. Then your answer is that we can eliminate using a coherently constant function .

Question: We know that we can eliminate using any weakly constant function (so that we don’t need to give all coherence data when ). There are at least two explanations of this. Does your work give a third explanation?

Your comment about coherently constant functions is exactly right.

To answer your question: Yes! I do not know either of the other two explanations, so I can’t compare my argument with them. Can you provide a link?

Using this construction: Suppose we’re given a weakly constant function . This corresponds exactly to a function . By functoriality of we get a map and similarly by induction a map . These maps do indeed form a cocone, the equality is true by reflexivity. So this gives a map .

Nice again! Just a corollary of your development.

Here are the links you want:

The first explanation is by Nicolai Kraus: The type of fixed points of any weakly constant endomap is a proposition,

http://www.cs.nott.ac.uk/~ngk/docs/hedberg.pdf,

from which the claim follows almost directly.

The second explanation is the same, with a different argument for the fact that the type of fixed points is a proposition, by Christian Sattler, recorded in page 19 of

Oh, this is great! (And thanks to Martin for giving the links to our previous work!)

Another question is this: Nicolai has an alternative notion of coherently constant function with the same elimination property: http://arxiv.org/abs/1411.2682

I wonder how this relates to your work.

Here is a comparison of the resulting universal property you get.

The disadvantage of my universal property is that it is “useless” when eliminating to -types. That is: the universal property is not easier when assuming that the codomain is an -type; you still have to construct a cocone over the whole diagram. In Nicolai’s work you only have to check finitely many things when eliminating to an -type.

Nicolai also had an idea where in the -th step of the diagram you only add -dimensional paths, so that becomes -connected. If that works, this gives a nice universal property when eliminating to -types.

The advantage of my work is that it is possible to formulate the general universal property (without assuming that the codomain is an -type) inside type theory, without assuming that the type theory has Reedy limits. And that it has been formalized in a proof assistant.

In neither case it is clear how useful the universal property is in applications; i.e. how bothersome it is to construct all the required data.

The universal property for eliminating to sets can be obtained by noting that . If it were true that as well, then that would also give a universal property for eliminating to -types; but it sounds from your comment like maybe that is not the case?

You’re right, for eliminating to sets this construction does work.

However, in this construction, is indeed not true for larger . At every step we’re adding new 1-paths, and only the next step corresponding 2-paths are added equating those 1-paths which are parallel, so is not -connected, even if it is inhabited.

Nicolai’s idea of an alternative construction (which I mentioned in my previous comment) will have this property, so can be used for this.

Intriguing. This seems kind of similar to my splitting-idempotents construction; in both cases we seem to get something “fully coherent” and involving paths of all dimensions without ever talking about anything above dimension 1. Of course we’ve seen that before, e.g. in the hub-and-spoke construction and even in Vladimir’s original definition of contractibility, but somehow it is more surprising to me that these two constructions work.

Ah, I have a better idea what’s happening now. For any there is a map which sends all the f-points to

baseand all the e-paths toloop. As long as A is inhabited, this map hitsloopwith an endo-path, which is therefore nontrivial. So there is no way could ever be 1-connected. And yet each new 1-path added in gets killed in , so in the colimit they all die. This makes the fact that the colimit ends up propositional more plausible to me than when I was imagining that the connectedness simply increases at every step.Yes, Floris’ construction is very clever at that point! So clever that I also found it surprising when I heard it the first time. But I do think that the approach where the connectedness increases at every step works as well (see my longer comment below). It’s true that the argument for that construction would be much easier if we had a “general Whitehead” at hand, but we can do it without (at least, that’s what I currently believe).

Maybe the conclusion to draw is that I still don’t really understand what the world looks like when Whitehead’s principle fails, for all that I talk about it a lot.

Here’s a possible test case for usefulness of these universal properties. In the proof of Lemma 8.2 in this paper (formalized in Coq here), I used the universal property for eliminating out of into sets. That necessitated a restriction in the lemma statement that be a family of sets (which was sufficient for what I needed at the time). But can the more general universal properties be used to generalize this lemma?

Oh, that’s interesting. I hope I can find some time to look at that. Thanks for the pointer.

Indeed, very nice! At first I didn’t think that this would work, because in general a type can be

n-connected for allnwithout being contractible; but somehow the sequential colimit takes care of that. I’m still dubious that one can get arbitrary localizations; does Egbert assume some kind of compactness of the generators?Another question: can your notion of “coherently constant function” be defined without using the one-step-truncation HIT, and if so, can one show directly that it suffices to eliminate from the propositional truncation?

You’re completely right about the localizations. Egbert assumes that the types for the localization are -compact. I clarified it in the article.

Your other question is interesting. I don’t know. To get it, you probably want to give the universal property of , but I don’t even see how to get the universal property of . I’ll think about it!

This is a very interesting construction, and a nice write-up!

For me, it’s especially interesting how you prove that is a mere proposition. I would have attempted to do it like this:

1. to show , it’s enough to show .

2. because is propositional, it is relatively easy to see that suffices.

3. given , we then want to show that is a centre of contraction.

That way, we really only need to do induction on one variable at a time. Maybe it could simplify things a tiny bit, but I think I understand why you didn’t do it: the easy case is if the two points in that we want to prove equal come from

the same, i.e. is much easier that . For comparison, in the other approach that you mentioned in the comments, this is not the case.(You have described very well what this approach is, but maybe it’s confusing to link between comments like this, so, let me quickly say what I mean. The approach for constructing truncations that Thorsten and I wanted to take is to start with , then take the 1-step [-1]truncation, then take the 1-step 0-truncation of the result, then take the 1-step 1-truncation of that result, and so on. Then, it’s really true that is the correct thing, so it would simplify if we want to eliminate into -types – but it’d probably be more complicated otherwise.)

I think I have a proof on paper for that construction, but at the moment not formalised and there could be all kind of flaws (maybe I’ll write a blog post, but only if I manage to find a nice presentation). This approach has its own difficulties, because even reducing the goal to won’t help much; I really need to go all the way down to , because “level zero” is the only time where we get actual equalities between

points.This idea is great! It doesn’t “simplify things a tiny bit”, it cuts the length my proof in half! If I can assume that is inhabited by , then I can choose as my center of contraction, and then I only have to worry about other points which are in a *higher* level than . So this makes the whole case obsolete. Moreover, there’s no need to induct on inequalities anymore, we can just induct on ordinary natural numbers. I implemented your proof strategy:

https://github.com/fpvandoorn/leansnippets/blob/master/short_prop_trunc.hlean

The proof that is a mere proposition went down from ~163 to ~76 lines.

I feel a bit stupid that I didn’t see this myself. I was already thinking that if I could assume that is inhabited, things would be easier. I also thought about your first step, but I didn’t see how assuming a point in could help: you cannot construct a point in or even from it. However, you can actually do that if you are proving only a mere proposition.

Great to see this implemented! I have used this strategy in a couple of other cases before, it’s often useful when you want to prove that some HIT is n-truncated.

The general strategy goes like this: To prove that is an -type (for ), it’s enough to show . But, if is some HIT, then you can show this by induction on , and, because you’re proving a mere proposition, all you need to check are the point-constructors. All higher constructors are automatic.

There are also some simple strategies to show something of the form (basically some higher versions of Hedberg’s argument), I have written about that in my thesis (Thm 3.2.1 summarises some of these “tools”, they are all trivial to prove; in Chp 8.10 in an application).

Does this technique make it easier to prove that is contractible (with either definition of )? (Luis Scoccola has recently submitted solutions to the two exercises in the book about this, 8.3 and 8.4.)

Good question, but I don’t see how it might help for (as a colimit). I think it’s the other way round: If you have a more difficult problem, you can try that strategy to reduce it to a problem which looks similar to “colimit – is contractible”. For example, in Floris’ construction, it essentially gives you this point in the “starting type” , and you already have such a point (or two) in the “starting type” . For “ as its own suspension”, I also don’t think it can be used.

I see. Too bad.

Pingback: The Lean Theorem Prover | Homotopy Type Theory

Pingback: Colimits in HoTT | Homotopy Type Theory

Pingback: Reflexive graph quotients are pushouts | Egbert RIJKE