The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible

The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible

Magic tricks are often entertaining, sometimes boring, and in some rarer cases astonishing. For me, the following trick belongs to the third type: the magician asks a volunteer in the audience to think of a natural number. The volunteer secretly chooses a number n. As a proof that he has really chosen a number, he offers to the magician x := ∣n∣, the propositional truncation of his number. The magician performs some calculations and reveals to the surprised volunteer that the number was n = 17.

When I noticed that this is possible I was at least as surprised as the volunteer: the propositional truncation ‖ℕ‖ of ℕ is a mere proposition, and I used to think that ∣_∣ : ℕ -> ‖ℕ‖ hides information.

So, how does this trick work? It is very simple: the magician just applies the inverse of |_| to x and the secret is revealed.

Of course, such an inverse cannot exists, but we can get surprisingly close. In this post, I show the construction of a term myst such that the following lines type-check:

  id-factored : ℕ -> ℕ
  id-factored = myst ∘ ∣_∣

  proof : (n : ℕ) -> id-factored n == n
  proof n = idp

The above code seems to show that the identity map on ℕ factors through ‖ℕ‖, but it becomes even better (or worse?): it factors judgmentally, in the sense that myst(∣n∣) is judgmentally equal to n (idp, for “identity path”, is the renamed version of refl in the new version of the Agda HoTT library).

My construction is not a cheat. Obviously, something strange is going on, but it is correct in the sense that if follows the rules of the book. It can directly be implemented in Agda, using the version of propositional truncation that is of the HoTT library, and I have a browser-viewable version on my homepage. For me, the most convincing argument of its correctness was given by Martin Escardo, who has checked that it still works in Agda if propositional truncation is implemented in the original Voevodsky-style (quantifying over all propositions). I have been very much inspired by Martin’s ideas on judgmental factorization of functions that have the same value everywhere (“constant” is a controversial name for these), and my own attempts to show that a factorization of such functions cannot be done in general. Both topics have been discussed on the mailing list before.

The construction of the “mysterious” term myst goes like this:
Let us say that a pointed type (X,x) is homogeneous if, for any point y : X, the pairs (X,y) and (X,x) are equal as pointed types. I think this means that X is contractible if we use heterogeneous equality instead of the usual one, but I prefer to call them homogeneous after a terminological remark by Martin.

I have two nontrivial classes of examples of homogeneous types: first, any type with decidable equality, equipped with a basepoint, is homogeneous; and second, any inhabited path space is homogeneous. Details (and the simple proofs) can be found in the above-linked Agda file. The natural numbers (equipped with any basepoint) which I have used in the examples above are included in the first class. If someone knows other examples, please let me know.

For a pointed type (X,x), let us write pathto (X,x) for the usual “Singleton” construction (an inhabitant of that type is a pointed type(Y,y), together with a proof that (Y,y) = (X,x) as pointed types). If (X,x) is homogeneous (with proof hom), we can define a function

  f : X -> pathto (X,x)
  f(y) = ((X,y) , hom (X,y)).

As the codomain is contractible, we can apply the recursion principle of the propositional truncation to construct

  f' : ‖X‖ -> pathto (X,x)
  f'(z) = recursor f z.

The computation rule of the truncation tells us that, for any y : X, the expressions f'(∣y∣) and ((X,y) , hom (X,y)) are judgmentally equal. Let us now define

  myst : ∏ ‖X‖ (fst ∘ fst ∘ f') 
  myst = snd ∘ fst ∘ f',

where fst and snd are the two projections. myst is thus a weird dependent function. Let us write E for (fst ∘ fst ∘ f'). The type of myst is then (in usual Agda notation):

  myst : (z : ‖X‖) -> E(z).

The crucial point that makes the whole construction work is that, whenever we plug in some ∣y∣ (for y : X), the expression E(∣y∣) reduces to X, and therefore, if we compose myst with the truncation map, Agda indeed believes us that the composition has type X -> X.

All the magician has to do for his trick is thus applying myst on the term x. For details, have a look at the end of my Agda file.

Note that the term myst is independent of the choice of proof of homogeneity. myst can thus be defined for any type and it will always reveal the secret that was hidden by ∣_∣. In general, we will not be able to prove homogeneity and myst will therefore be an open term, but the secret will be revealed nevertheless.

As ‖X‖ has the same points as X, only that there are paths added between any two points, it is actually not too surprising that ∣_∣ does a bad job at hiding. To summarize, all I have done is using that ∣y∣ has enough computational properties to identify it as ∣_∣ applied on y. I still think it is interesting and counterintuitive that we can make this idea concrete in a way that makes everything type-check.