Solve exercise 3.15 and 3.17

[HyunggyuJang]

No description provided.

[jdchristensen]

"on" should be "in", and the comment should end in a period.

@mikeshulman Do you think this comment is sufficient, or should the exercise explicitly use universes and propositional resizing? (I said a bit more about what this would entail in another comment.)

[HyunggyuJang]

Got it; for now let me fix the preposition.

[mikeshulman]

I think it would be better to use universes and propresizing explicitly. But we could merge this now and potentially make that improvement later.

[jdchristensen]

In case @HyunggyuJang isn't familiar with using propositional resizing, here is one way to start the solution:

  Definition Book_3_15_trunc@{u +} `{PropResizing} `{Funext} (A : Type@{u})
    : Type@{u}.
  Proof.
    exact (resize_hprop@{_ u} (forall P : HProp@{u}, (A -> P) -> P)).
  Defined.

  Definition Book_3_15_ishprop `{PropResizing} `{Funext} (A : Type)
    : IsHProp (Book_3_15_trunc A)
    := _.

Also note that the existing solution didn't actually state that the type is a proposition, so I added that as well. The rest will be essentially the same, but all results will need both propositional resizing and Funext.

[HyunggyuJang]

Thanks a lot for your detailed instruction, @jdchristensen. Yes, I'm not that familiar with propositional resizing, so let me just apply your instruction ASAP; besides that, I learned a lot from your comments, much appreciated, @jdchristensen!

[HyunggyuJang]

Reflected at 2b657ab
Note that, in Coq, we cannot express judgemental equality unlike the note in the text; I added a remark for it. @jdchristensen @mikeshulman Can you check whether it is appropriate?

[Alizter]

One way to express "judgemental equality" is to assert two terms as equal by a path and explicitly set the proof to idpath.

[HyunggyuJang]

@Alizter Thanks for your remark. Indeed I expressed judgemental equality with reflexivity tactic at https://github.com/HoTT/Coq-HoTT/pull/1678/files/da9b3099387a692ba7bd1c44620b869e01b5be2a..09102873e3e89f34087adaa752958132b97307b3#diff-ff4b6a1211719941834f9aec6bc57ef7b3203e603479e0ad60353086b6b0fe25R956
Think what you said and the way I expressed it are basically the same.

[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.