Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Solve exercise 3.15 and 3.17 #1678

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Solve exercise 3.15 and 3.17 #1678

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
da9b309
Solve exercise 3.15 and 3.17
HyunggyuJang Nov 4, 2022
0910287
Reflect reviews
HyunggyuJang Nov 30, 2022
fea4f10
Reflect review
HyunggyuJang Nov 30, 2022
2b657ab
Make propositional resizing assumption explicit
HyunggyuJang Dec 2, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions contrib/HoTTBookExercises.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -940,6 +940,7 @@ End Book_3_14.
(** Exercise 3.15 *)

Section Book_3_15.
(* Propositional resizing is (implicitly) used for [forall P : HProp, (A -> P) -> P] to be on the same universe as [A] *)
Copy link
Collaborator

@jdchristensen jdchristensen Nov 30, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"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.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Got it; for now let me fix the preposition.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

Copy link
Contributor Author

@HyunggyuJang HyunggyuJang Dec 2, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

@Alizter Alizter Dec 2, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Definition Book_3_15_rec {A B} `{IsHProp B}
: (A -> B) -> (forall P : HProp, (A -> P) -> P) -> B.
Proof.
Expand All @@ -954,7 +955,6 @@ Section Book_3_15.
Proof.
intro a. reflexivity.
Qed.
(* proportional resizing is needed? *)
End Book_3_15.

(* ================================================== ex:lem-impl-dn-commutes *)
Expand All @@ -968,12 +968,11 @@ End Book_3_15.
Section Book_3_17.
Theorem prop_trunc_ind
: forall A (B : merely A -> Type),
(forall a, B (tr a))
-> (forall x, IsHProp (B x))
(forall x, IsHProp (B x))
-> (forall a, B (tr a))
-> forall x, B x.
Proof.
intros A B base p x.
specialize (p x).
intros A B p base x.
refine (Trunc_rec _ x).
intro a.
assert (H: tr a = x) by (apply path_ishprop).
Expand Down