Exercise 3.15 on impredicative truncation

[jdchristensen]

Exercise 3.15 asks the reader to define propositional truncation using \Pi_P ((A -> P) -> P) with propositional resizing, and to show that the computation rule is judgmental. In Coq-HoTT, this is formalized in https://github.com/HoTT/Coq-HoTT/blob/master/theories/Metatheory/ImpredicativeTruncation.v, but we only get a propositional computation rule. Is there a different way to do this can gives a judgmental computation rule, or should the exercise be changed?

[awodey]

it seems to me, too, that the computation rule will only be propositional.

[mikeshulman]

The exercise says to show that it has the same recursion principle with the judgmental computation rule. Isn't that what Trm_rec_beta in the Coq file shows?

[mikeshulman]

I guess it is a bit unclear because the exercise says "if we assume propositional resizing" but then it states a property of a type that lies in a higher universe and is not resized. I think the type stated in the exercise does have a judgmental computation rule for the recursion principle, but after we resize it to an equivalent type in the same universe as A, it will only have a propositional computation rule. Is that the point?

[jdchristensen]

The Coq-HoTT file I linked to does it three ways. First, without resizing, and having the result be in a different universe. Then you get a judgmental computation rule. Then it gives two ways to make things land in the right universe. One is to resize the propositions that you use as motives for the rule. With this approach, you are literally using the proposed definition of the truncation, but you still only get a propositional computation rule. A second approach is to use resizing on the proposed definition of the truncation. This requires Funext for the definition, so I don't like it as much, and in any case you still only get a propositional truncation rule. (The formalization of this last way does resizing on both the definition of the truncation and on the motive of the truncation, but even if it only did the former, you still wouldn't get a judgmental computation rule.)

So at the very least I'd say the exercise is misleading. But if you are really trying to define an operation that lands in the same universe, I don't see a way to get a judgmental computation rule, so I think the exercise should say that.

[jdchristensen]

(And just to get clear, the exercise doesn't specify how the universe of P relates to the universe of A. If you choose the Ps to run over a smaller universe, then the proposed definition does land in the same universe as A, and so doesn't need to be resized. This is how the second of the three methods in ImpredicativeTruncation.v does it. The only quibble with that method is that A can't be in the lowest universe.)

[mikeshulman]

Yes, I agree the exercise is misleading. One possibility would be to give it two parts:

(a) For $A:U$, show that $\prod_{P:\mathrm{Prop}_U} (A\to P) \to P$ has the same recursion principle as $\Vert A \Vert$, with judgmental computation rule.

(b) The type in the previous part does not lie in the same universe U. Show that if we assume propositional resizing, we can define a type in the same universe as A and satisfying the same recursion principle as the propositional resizing, albeit only with a propositional computation rule.

[jdchristensen]

That looks good to me!

[mikeshulman]

Another point is that the recursion principle with judgmental computation rule applies only to motive propostions that lie in the same universe, whereas the true propositional truncation can eliminate into propositions in any universe.