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

Posted on 28 October 2013 by Nicolai Kraus

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.

About Nicolai Kraus

At the University of Nottingham

View all posts by Nicolai Kraus →

This entry was posted in Code, Higher Inductive Types. Bookmark the permalink.

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

Andrej Bauer says:

28 October 2013 at 13:33

I would imagine that a (dependent) product of a family of homogenous types is homogenous, which immediately gives you many examples. A group ought to be homogenous, because an equivalence from $(G, x)$ to $(G, y)$ is given by $\lambda z : G . y x^{-1} z$ . Thus the real numbers, vector spaces, etc., are homogenous. Interestingly, we cannot expect a set to be homogenous, but surely a cardinal number would turn out to be homogenous?

Reply
- jessemckeown says:
  
  28 October 2013 at 20:20
  
  so … are cardinals cofibrant? My long habit of thinking that cardinals are special ordinals would discourage me from such a hope, but you probably have some other notion of cardinal in mind.
  
  Reply
- Martin Escardo says:
  
  29 October 2013 at 05:10
  
  Any type (including a set) admitting a group action should be homogeneous.
  https://en.wikipedia.org/wiki/Homogeneous_space
  Also, all the “simple types” (start with N and close under -> and x) are homogeneous. And there are other obvious closure properties of homogeneous types.
  
  Reply
  - jessemckeown says:
    
    29 October 2013 at 09:41
    
    *transitive* action. *Internally* transitive.
    
    Reply
- Nicolai Kraus says:
  
  29 October 2013 at 11:31
  
  Great! Indeed, if $B$ is a family of homogeneous types over some (ordinary) type $A$ , then $\Pi_A B$ is homogeneous, and similar for the special cases $\times$ and $\rightarrow$ . I don’t understand what it means for cardinals though. In the book, a cardinal is an element of the 0-truncation of the universe of sets. The property of being homogeneous is not a set, so how can it be defined for a cardinal? Does someone see how this can be done?
  
  Reply
  - Peter LeFanu Lumsdaine says:
    
    29 October 2013 at 12:53
    
    Yes, I’m also not seeing what Andrej means by “cardinal number” above. If he means a cardinal-finite set $\{x_1,\ldots,x_n\}$ , then certainly it’s homogeneous: just use the obvious swap of elements. If he means an element of the 0-truncation of Sets, then a cardinal can no longer be seen as a type-with-extra-properties, so it’s not clear what it means for one to be homogeneous.
    
    Reply
    - Andrej Bauer says:
      
      18 April 2015 at 09:44
      
      I can’t tell what Andrej meant either.
      
      Reply
Daniel R. Grayson says:

28 October 2013 at 16:29

The loop space Omega(X,x) should be homogeneous, too.

Reply
- Nicolai Kraus says:
  
  29 October 2013 at 13:37
  
  Yes, that’s true! In fact, I was thinking about that example when I noticed that something interesting is going on. (I had the loop space in mind when I wrote “inhabited path space”, but that was not a good way to express it.)
  
  Reply
Twan van Laarhoven says:

28 October 2013 at 19:02

Wow, that’s unexpected.
Since ‖ℕ‖ is a -1 type, you have that |1| == |0|, shouldn’t that mean that mean that myst |1| == myst |0|, and because therefore by transitivity that 1 == 0?

But now that I write this, I realized that what you actually get out is a heterogeneous equality. myst |1| =[ x ]= msyt |0|, so also 1 =[ y ]= 0, for some x and y; where I write x =[ e ]= y for the equality cast e x == y. And 1 =[ y ]= 0 is not that hard to prove using an univalance to construct an equality that swaps 0 and 1.

Reply
- Guillaume Brunerie says:
  
  28 October 2013 at 19:44
  
  … and this equality that swaps 0 and 1 is exactly what Nicolai is constructing using the fact that N is homogeneous.
  
  Nicolai: That’s very nice 🙂 It shows that we really cannot erase hpropositions in the same way we can erase propositions in Coq.
  
  Reply
  - Arnaud Spiwack says:
    
    29 October 2013 at 05:18
    
    Non-erasability is probably a consequence of unique choice: it’s not because there is only one element that you can guess it. An obvious example would be equivalences, certainly there is at most one inverse to a function f, but I cannot deduce it from g.
    
    It’s touted as a good thing in the HoTT book. I’m still quite doubtful about that though. I find erasability a useful property (but there are surely other ways to get erasability).
    
    I like how it is another demonstration about how tricky identity types are. When you want to prove that 0 = 1 from this, you’ll get stuck, if I’m not mistaken, at some illegally typed generalisation which is not obvious on a pen and paper proof. I’m wondering, by the way, if the existence of myst is sufficient to disprove K.
    
    Reply
    - Peter LeFanu Lumsdaine says:
      
      29 October 2013 at 09:36
      
      I’m wondering, by the way, if the existence of myst is sufficient to disprove K.
      
      Yep, it is! The existence of $\mathsf{myst}$ for a type $X$ implies that given any $x_0:X$ , we get $X$ as a retract of $X=X$ . In particular, if K/UIP holds, then $\mathsf{myst}$ can only exist for props.
      
      By “existence of $\mathsf{myst}$ ”, I mean precisely: a function $F : \|X\| \to \mathsf{Type}$ , and $f : (y : \|Z\|) \to F(y)$ , with $\varphi : (x : X) \to F(|x|) = X$ , and $\psi : (x : X) \to f(|x|) =_{\varphi(x)} X$ . In Nicolai’s case, $\varphi$ and $\psi$ are both judgementalised, but of course we can’t take that as an assumption.
      
      Anyhow, in this situation, fix some $x_0:X$ . Now for each other $x:X$ , we can apply $\mathsf{apd} f$ , together with some fiddling with transport, to get an equality $x = _{\varphi(x)^{-1} \cdot \mathsf{apd}(?) \cdot \psi(x_0)} x_0$ (where $?$ is the canonical path $|x| = |x_0|$ ).
      
      This exhibits $X$ as a retract of $X=X$ , via the maps $x:X \mapsto \varphi(x)^{-1} \cdot \mathsf{apd}(?) \cdot \psi(x_0)$ , and $p:(X=X) \mapsto p_* x_0$ .
      
      Reply
    - Nicolai Kraus says:
      
      29 October 2013 at 12:09
      
      Twan: Yes, indeed: we don’t get 0 = 1, we only get that 0, *if we transport it along some proof that 0 and 1 live in the same type*, is equal to 1. The confusing thing is that 0 and 1 “accidently” already live in the same type anyway.
      
      Guillaume: Thanks! I also had to think of the erasing-thing.
      Actually, if we want to erase something, we require it to not have any importance for the future computation. But that is very different from “being an inhabitant of a proposition”. The term ∣n∣ has as many computational properties as n itself has. “Being a proposition” might be a prerequesite for “containing only erasable information” though, but I don’t have a good understanding of the whole idea of erasing at all. Isn’t it just for efficiency of implementations, or am I missing something?
      
      Arnaud: About the K-question, there is not much to add to Peter’s perfect answer.
      This is probably obvious (and it does not match your question), but already the statement that ℕ is homogeneous contradicts K: this statement implies that 0, if transported along a proof of ℕ = ℕ, is 1; and K would allow us to assume that this proof is the trivial one. If we do that, what we have really becomes a proof of 0 = 1.
      
      Reply
      - Peter LeFanu Lumsdaine says:
        
        29 October 2013 at 13:00
        
        …already the statement that ℕ is homogeneous contradicts K.
        
        This is a slightly slippery statement. Certainly, with “homogeneous” defined the way it is here, it’s true. But working without univalence, as presumably we are if we’re asking “does such-and-such contradict K”, one would surely define homogeneity slightly differently, as “for all $x,y:X$ , there is some automorphism of $X$ sending $x$ to $y$ ”. (Under univalence, these definitions are of course equivalent.) And with that definition, ℕ and the various other examples become provably homogeneous again — no contradiction with K.
        
        Indeed, homogeneity (defined this second way) seems like a rather interesting property even without univalence or the homotopy PoV. Have constructivists studied it before?
        
        Reply
jessemckeown says:

28 October 2013 at 20:03

In ordinary homotopy, we should expect a space to be homogeneous in the present sense whenever all path components are equivalent and cofibrantly included. This is probably where Daniel got his examples.

Reply
- jessemckeown says:
  
  28 October 2013 at 20:37
  
  Oh, now I see you meant “∀ y : X , (X, x) = (X, y)” rather than “∀ y : X , || (X , x) = (X, y) ||”. This feels trickier; they should mean the same thing for decidable-equality spaces, but not generally. The former says the total space of the tautological fibration over the classifier for Aut (X) is contractible, which means it says X is a loopspace; that is, Daniel’s examples are essentially all of them.
  
  … it’s a good thing there are groups of every cardinality. But I don’t suppose coq or agda can be convinced of this?
  
  Reply
  - jessemckeown says:
    
    29 October 2013 at 00:59
    
    I take that back, it’s not that the total space of that thing is contractible (that almost never happens…). It really is “homogeneous”, in the sense that X is a retract of Aut(X), that there is a section of the map $\mathrm{ev}_x : f \mapsto f ( x )$ .
    
    Reply
Peter LeFanu Lumsdaine says:

28 October 2013 at 23:07

This is extremely nice, and somewhat unsettling! I’m still finding it slightly hard to come to terms with — it really feels like it should lead to a contradiction somehow. One realisation that I found helpful was to pin down the source of my discomfort as the apparent contradiction “We have $\mathrm{id}_\mathbb{N} = f \circ g$ , so the identity factors through a constant map; doesn’t that make the identity constant?”

The resolution of this is that $f \circ g$ here doesn’t factor through $g$ in the usual sense! Being careful about our definitions, a map $h : X \to Z$ factors through $g : X \to Y$ if there’s some $f : Y \to Z$ such that $h = f \cdot g$ . (And with this, we can indeed prove that if $h$ factors through a constant function, $h$ is constant.) In our case, we do have $h = f \cdot g$ , but $f$ isn’t a simple function, it’s a dependent function $f : (y:Y) \to F(y)$ , where it just happens to be the case that $F(g(x)) = Z$ .

So the proposed contradiction above doesn’t typecheck; and trying to go through its argument with the specifics in this case, we get exactly Guillaume’s point, that the equality between $|x|$ and $|y|$ maps not to an equality between $x$ and $y$ but between some transport of $x$ and $y$ .

This still makes me deeply uncomfortable, though. It really feels like something is being retained that shouldn’t be…

Reply
- jessemckeown says:
  
  29 October 2013 at 00:55
  
  Maybe we need a “no-knowledge proof” semantics for truncation… But I’m not sure there’s more here than an argument that the inclusion of X in (our agda model of) ||X|| is a cofibration, in some sense.
  
  Or else, is this perhaps an instance of the … I can’t remember who found the issue. Dan Licata’s name popped into my head, but I don’t remember if it was him or someone else… the issue that oops theorems which were easy to write in coq back then were actually also definable in contemporary agda, and so the agda developers put together some patch, but… yeah, I can’t remember and don’t know who’s responsible, but other people here will know.
  
  Reply
- Nicolai Kraus says:
  
  29 October 2013 at 12:35
  
  Peter: Thank you! I also feel strange about this; apparently, ∣_∣ just “changes the type” of something that you apply it to, but nothing else and, in particular, no information is “lost”. The thing that allows me to accept it is that this whole statement is meta-theoretic. Internally, the world is still okay – ‖X‖ is propositional and we cannot get a function ‖X‖ -> X with a non-expected property (we can get one that is just constantly the basepoint of X, which exists by definition of homogeneity, but that’s fine).
  I can imagine that (judgmental) computation rules for HITs have a bunch of other weird and (at first) counter-intuitive consequences which we will discover sooner or later! (When we did the “Generalizations of Hedberg’s Theorem”-project, we assumed a theory without the judgmental computation rule for truncation, and such a weakened form of truncation is already very useful. If I am not mistaken, in that case it is also safe to “erase” terms of type ‖X‖. It is certainly not a desirable thing to only have “weak” HITs though.)
  
  Reply
  - Martin Escardo says:
    
    29 October 2013 at 13:23
    
    Two remarks. (1) The puzzle comes from the fact that for any closed term t : N, the type E t reduces to N, and hence myst | t | = t is possible. But if t is a variable of type N, the type of myst | x | is not N (it is some strange type E x that doesn’t reduce to N). Intuitively, this is saying you can do the revealing trick for each definable (or postulated) natural number, but not in a “continuous” or “natural” way for all natural numbers. Or this can be seen in another way: the only way you can possibly define closed term of type ||N|| is by first defining some n and then taking |n|. And this doesn’t seem unresonable. (2) I think that even in the weak form of truncation you cannot erase terms of type ||X||. Indeed, consider the case already discussed in the mailing list, that ||Sigma x : N. f x = 0|| -> Sigma x : N. f x = 0, for any f:N->N. If you have a closed term t for the premise, and erase it, how are going to get the x:N of the conclusion? The thing is that although hpropositions may have all inhabitants equal, this doesn’t mean that the inhabitants don’t have computational content. To stress this point, consider “there is a minimal x: N, f x=0”. This now is an hproposition, which clearly does have computational content: if you erase a term witnessing that or the truncation of that, you will get into trouble. Information can leak from ||X|| to any hproposition P, and the essence of your trick is that an homogenous X allows you to get a suitable P for your job. But you also rely on the judgemental equations for the definition of ||-||, as you seem to be hinting.
    
    Reply
    - Peter LeFanu Lumsdaine says:
      
      29 October 2013 at 13:48
      
      But if t is a variable of type ℕ, the type of myst | x | is not ℕ (it is some strange type E x that doesn’t reduce to ℕ).
      
      Really? If I’m following right, the really slick part of the trick is that the type does reduce for an arbitrary variable $x : \mathbb{N}$ . (And this is necessary for $\mathsf{myst} \cdot |-|$ to typecheck as a function $\mathbb{N} \to \mathbb{N}$ .)
      
      What doesn’t, and can’t, reduce to $\mathbb{N}$ is the type of $\mathsf{myst}(y)$ for arbitrary $y : \|\mathbb{N}\|$ . We can prove that for all $y$ this type is equal to $\mathbb{N}$ ; but not by an equality which will be equal to $\mathsf{idp}$ whenever $y = |x|$ , since if we had that, then we would actually get the threatened contradiction of the identity map factoring through a constant map.
      
      Reply
      - Martin says:
        
        29 October 2013 at 15:18
        
        Sorry, I meant to say for t : ||N||, so that you can write myst t so that you know what it was. If you write E |x|, that does normalize to N. But if you write E s where s is a variable of type s:||N||, then it doesn’t normalize to N.
        
        Reply
    - Nicolai Kraus says:
      
      29 October 2013 at 15:53
      
      (2) I think that even in the weak form of truncation you cannot erase terms of type ||X||. Indeed, consider the case already discussed in the mailing list, that ||Sigma x : N. f x = 0|| -> Sigma x : N. f x = 0, for any f:N->N. If you have a closed term t for the premise, and erase it, how are going to get the x:N of the conclusion?
      
      The disagreement probably comes from the fact that I don’t know what “erasability” means 🙂
      What I meant in my comment is that, if we don’t assume the computation rules for truncation, we can ignore an inhabitant of ‖X‖ for the whole computation; i.e. we can replace it by some “hole” and it makes no difference for the computation. I did not mean that you can “forget it and just reconstruct it later” (that is nearly never the case I guess). But, about your question of how to get $x : \mathbb{N}$ : the point is that you won’t get an actual (canonical) natural number, no matter whether you erase or keep the inhabitant of ‖…‖, it just won’t compute. For other propositions it is not true that you can erase their inhabitants in that sense, because, as you say, they might as well have computational content.
      
      Reply
- spitters37 says:
  
  29 October 2013 at 15:35
  
  As Arnaud says we already knew that we had unique choice in HoTT, so something needs to be retained. Moreover, although this “inverse” is surprising, of course we cannot print “17”, so the analogy with the magician is a bit broken.
  
  Still it is a nice result.
  
  Reply
  - Nicolai Kraus says:
    
    29 October 2013 at 15:43
    
    What do you mean by “of course we cannot print 17”? Yes, we can – and that is the point of my post 😉
    
    Reply
    - spitters37 says:
      
      30 October 2013 at 04:03
      
      I see now. Cool trick!
      
      Reply
Martin Escardo says:

29 October 2013 at 05:28

Just for the record, the “judgementalization” operation mentioned in Nicolai’s post is here:
http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#14905

Suppose you have a constant function f:X->Y (in the sense that any two values of f are connected by a path) that factors through |-|:||X||->X. From any factor f’:||X||->Y you can construct another factor f”:||X||->Y such that the path f o |-| = f” is refl. Here ||-|| is -1-truncation.

Reply
- Martin Escardo says:
  
  29 October 2013 at 05:38
  
  Of course I meant such that the path f” o |-| = f is refl.
  
  Reply
Andrea Vezzosi says:

29 October 2013 at 08:18

Could you also share the plain .agda files?

I’d like to see what happens if we try to prove E(z) = const X

Reply
- Andrea Vezzosi says:
  
  29 October 2013 at 08:19
  
  E(z) = X or E = const X, actually.
  
  Reply
- Nicolai Kraus says:
  
  29 October 2013 at 11:16
  
  Yes, I have been wondering what the best way to do this would be – not only for this Agda file, but in general. I don’t maintain a public git repository so far. Maybe we could create some folder in the HoTT-Agda part of the community git repository where things like this could be shared?
  For now, I have put the file here: trunc-inverse.lagda.
  It uses the HoTT library: 2.0 branch.
  
  Reply
Mike Shulman says:

29 October 2013 at 15:08

Cute! I had the same initial reaction as PLL: “that can’t possibly be right”. But now I think I see how it works. Calling this a “magic trick” is very appropriate: it seems to be doing one thing, but is actually doing something slightly different, and there’s a subtle bit swept under the carpet.

Here’s how I would explain the trick to a category theorist. Saying that the identity map of $\mathbb{N}$ factors through $\Vert\mathbb{N}\Vert = 1$ would say that we have a map $f:1\to \mathbb{N}$ such that $f\circ g = \mathrm{id}_{\mathbb{N}}$ . Clearly it would suffice to instead have a map $f:1\to Y$ , for some countably infinite set $Y$ , such that for some isomorphism $Y\cong \mathbb{N}$ we obtain the composite $\mathbb{N}\to 1 \to Y \cong \mathbb{N}$ being the identity. But if there’s a canonical such isomorphism, then we might decline to notate it.

Now a map $f:1\to Y$ induces of course a map $(\mathrm{id},f):\mathbb{N} \to \mathbb{N}\times Y$ , and we obtain the composite $\mathbb{N}\to 1 \to Y$ by composing $(\mathrm{id},f)$ with the second projection. I think what’s happening in your proof, from this perspective, is the construction of a particularly clever countably infinite set $Y$ such that each fiber of $\mathbb{N}\times Y$ is canonically isomorphic to $\mathbb{N}$ , but by an isomorphism that is different in each fiber. Therefore, after projecting to get the map $\mathbb{N}\to 1 \to Y$ , we apply a different isomorphism $Y \cong \mathbb{N}$ at each input value $n:\mathbb{N}$ , thereby obtaining $n$ again as the output. Finally, since these canonical isomorphisms are in fact judgmental equalities, the fact that we are passing back and forth across them gets swept under the rug and it looks like magic is happening.

Reply
- Nicolai Kraus says:
  
  29 October 2013 at 16:08
  
  Thanks for the translation – also, excellent phrasing in the first paragraph, I like it!
  
  Reply
Michele Morelli says:

3 November 2013 at 14:39

Very nice! My intuition for it is that if when we take $X$ as a pointed space, if the point is irrelevant (i.e., $\forall x . \forall y . (X, x) = (X, y)$ ), then $(X, x)$ should behave similarly enough to $\Vert X \Vert$ , since one point is as good as another, and $\Vert X \Vert$ is like a pointed X in which we don’t know the point. So, when the point is irrelevant it can be extracted, that makes sense.

But one thing is not clear to me. You said:

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.

Which is true, myst never uses *directly* the proof of homogeneity, but isn’t it still needed to construct f-lifted (as named in the Agda code) by truncation induction? I don’t see how the construction could go through without f-lifted. If we can’t construct myst, how do we reveal the secret?

Reply
- Nicolai Kraus says:
  
  3 November 2013 at 16:05
  
  Thanks! – My statement was mistakable. What I wanted to say is that the proof of homogeneity has no influence on the computation. The composition myst ∘ ∣_∣ is pointwise judgmentally equal to the identity map even if we do not have the proof of homogeneity (i.e. if Agda has a hole where the proof should be) – that is why I said that myst would be an “open” term. For the magician in the first paragraph, it does not matter whether or not ℕ is homogeneous, he could have done the trick with any type. The audience does not know whether there are holes in the Agda file, they only want to see whether the magician can find the “hidden” element. He can use the term myst to reveal the secret even if not all components of this term can actually be constructed. You are right that we cannot construct the complete term myst without homogeneity but we can construct enough of it to get the meta-theoretic result that ∣_∣ is not safe if we want to hide an element.
  
  Reply
  - Michele Morelli says:
    
    4 November 2013 at 08:59
    
    While it doesn’t directly affect the computation, it *is* necessary to construct myst, else we can’t get the map $f' \Vert X \Vert \to \mathrm{pathto} (\mathrm{base}, \mathrm{pt})$ from which it is defined, right? If $f : X \to \mathrm{pathto} (\mathrm{base}, \mathrm{pt})$ alone sufficed, by a similar argument, $\mathrm{trunc-choice} : (\forall x . \Vert \exists y . R(x,y) \Vert) \to \Vert \exists f . \forall x . R(x,f(x))$ would be provable by a similar argument, but you get stuck when trying to satisfy the path constructor case of truncation that just isn’t provable, and this is what should also happen when trying to construct $f'$ without homogeneity.
    For this reason, I think that Agda extracting $x$ from $|x|$ when instead of a proof you have an hole should be regarded more as a “bug”, the same kind of “bug” you get by implementing Markov’s principle $(\forall x . P(x) \lor \neg P(x)) \to \neg \neg (\exists x . P(x)) \to \exists x . P(x)$ by turning temporarily off the termination checker and then calling it with a hole for the $\neg\neg\exists$ argument, which computationally is never used, when in fact it’s provably not true. The result is non-termination, but I wouldn’t say it’s MP’s fault, rather the hole’s fault. Of course we can’t completely blame Agda here, we’re making it do more than what it’s designed to do safely.
    
    Lastly, I agree that $|x|$ can’t erase the $x$ in some cases, but I’m not so sure for non-homogeneous types.
    
    Reply
    - Michele Morelli says:
      
      4 November 2013 at 09:02
      
      Sigh. I really wish wordpress had a preview button for comments…
      
      Reply
    - Nicolai Kraus says:
      
      4 November 2013 at 14:07
      
      Well, I made a couple of different statements in the post. The statement I made in the paragraph that you cited was meta-theoretic: ∣x∣ has as many computational properties as x so that one can find x, possibly only with cheating (not proving everything). It does not make sense to view this as an internal statement. It is something I say about the theory, not in the theory. What makes it confusing is that myst, viewed as a meta-theoretic algorithm to “undo” the operation ∣-∣, is (in the example of ℕ) a definable term in the theory. What I meant is that it still works, even if it is not a definable term. The whole result that we can find x from ∣x∣ up to judgmental/definitional equality cannot be expressed internally!
      
      In contrast, what you discuss is completely internal to the theory. Let’s say we use some axiom that makes the theory inconsistent. Then, we can easily prove trunc-choice. If there is a “hidden” z : X and we can only see x := ∣z∣, we can (using the inconsistency) easily produce some y : X and a proof that y = z. However, it is still surprising that we can find z up to definitional equality, that is something that you cannot get for free from a contradiction – because it cannot be expressed internally.
      
      I would certainly not view it as a “bug” that Agda does computation before all holes are filled. If it did not do that, using Agda would be really, really painful. You would only be able to ask Agda whether some expression type checks when your program does not have any gaps any more (maybe when it’s already done).
      
      In practice, if you agree that Agda is not allowed to erase for homogeneous types, you will probably not want to erase at all anyway. Whether a type is homogeneous or not depends on the assumptions that you currently have (including the axioms you use). Agda will never be able to know for sure that it is allowed to erase.
      
      Reply
      - Michele Morelli says:
        
        4 November 2013 at 15:08
        
        I don’t feel like we’re disagreeing here. $|x|$ has to keep the $x$ around somewhere, since you don’t know what you can and cannot erase. Cheating would still be cheating, though.
        
        I called it a “bug” for lack of a better word, the bug is really on our end rather than Agda’s, it’s us that had to be careful with putting holes in improper places.
        
        Reply
Mike Shulman says:

4 November 2013 at 14:14

I have to say that this trick makes me a bit more suspicious of all judgmental equalities. Maybe even beta-reduction should be propositional.

Reply
anka213 says:

7 September 2022 at 04:17

I’m getting this error when trying to open http://www.cs.nott.ac.uk/~psxngk/html-trunc-inverse/trunc-inverse.html
> No access to directory.

> The Computer Science web server is available to current Computer Science Staff and Research students.
> If you believe you are seeing this message in error, please contact the support team.

Reply
- Nicolai Kraus says:
  
  7 September 2022 at 04:44
  
  That’s because the university disabled my student webpage when I graduated. It’s not here:
  http://www.cs.nott.ac.uk/~psznk/docs/html-trunc-inverse/trunc-inverse.html
  
  Reply
  - Nicolai Kraus says:
    
    7 September 2022 at 04:56
    
    *now
    
    Reply