Solve exercise 3.15 and 3.17

[HyunggyuJang]

[mikeshulman]

(Moving the discussion out of the inline comments on an out-of-date line.)

With apologies to Dan who made this suggestion, I don't think this is quite what the exercise means. It doesn't say to prove that a resized version of forall (P:Prop), (A -> P) -> P has the recursion principle, but that forall (P:Prop), (A -> P) -> P itself has that principle. Propositional resizing should be used instead on the proposition you're eliminating into, to move it down into the right universe. (The current version doesn't, I think, prove that the recursion principle can map into a proposition in an arbitrary universe, but probably collapses the universes of A and B to be the same.)

However, I do also think you've found a mistake in the book. Even doing it the way I suggest, I think you're only going to get a typal computation rule, for essentially the same reason. And the book's propositional resizing is no stricter than the one in Coq, so it should also only have a typal computation rule.

[HyunggyuJang]

(Moving the discussion out of the inline comments on an out-of-date line.)

With apologies to Dan who made this suggestion, I don't think this is quite what the exercise means. It doesn't say to prove that a resized version of forall (P:Prop), (A -> P) -> P has the recursion principle, but that forall (P:Prop), (A -> P) -> P itself has that principle. Propositional resizing should be used instead on the proposition you're eliminating into, to move it down into the right universe. (The current version doesn't, I think, prove that the recursion principle can map into a proposition in an arbitrary universe, but probably collapses the universes of A and B to be the same.)

However, I do also think you've found a mistake in the book. Even doing it the way I suggest, I think you're only going to get a typal computation rule, for essentially the same reason. And the book's propositional resizing is no stricter than the one in Coq, so it should also only have a typal computation rule.

Thanks for your detailed remark. I’ll try to reflect your point. So basically, should encode the truncation as forall (P:Prop), (A -> P) -> P, then use propositional resizing to adjust P to be in the proper universe. Got it.

[jdchristensen]

Oh, sorry for the misunderstanding. I had assumed that the idea was to show that for any universe, you get a modality on that universe. Now I see what was meant. Hopefully my example of using PropResizing is still helpful.

[jdchristensen]

@HyunggyuJang This was a tricky task and I'm not exactly sure what the current state is, but are you interested in reviving this PR? I'm happy to help.