Lemmas 3.3.2 and 3.3.3 and Exc. 3.9

Lemmas 3.3.2 and 3.3.3 added to HProp
Backrefs added to HoTTBook
Solution to Exc.3.9 added to HoTTBookExercises


I would be interested to hear more about @marcbezem's experience, but I
think for me personally, the problem would not be a failure to say `apply
path_hprop` but rather confusion resulting from the goal not appearing to
change when I do apply it.  My thought process would be "okay, I have to
construct a path between two elements of `hProp`, so I'll use `path_hprop`
to reduce the problem to constructing a path between types, which I know
how to do... but that doesn't seem to have worked, because Coq is still
asking me to construct a path between two elements of `hProp`!  Help!"

On Wed, Oct 1, 2014 at 2:19 PM, Jason Gross <notifications@github.com>
wrote:

> In contrib/HoTTBookExercises.v:
>
> > +Proof.
> > +  intro lem.
> > +  apply (equiv_adjointify (LEM_hProp_Bool lem) is_true).
> > +  unfold Sect. intro b. destruct b; simpl.
> > +  unfold LEM_hProp_Bool. elim (lem Unit_hp _).
> > +  exact (fun _ => 1).
> > +  intro nUnit. elim (nUnit tt).
> > +  unfold LEM_hProp_Bool. elim (lem False_hp _).
> > +  intro fals. elim fals.
> > +  exact (fun _ => 1).
> > +  unfold Sect. intro hprop.
> > +  elim (lem hprop _).
> > +  intro p.
> > +  unfold LEM_hProp_Bool. elim (lem hprop _). simpl.
> > +  intro useless.
> > +  apply path_hprop. simpl.
>
> My suggestions/ideas are:
> For people reading the proof:
> Have Open Scope long_type_scope and a comment about it. This should make apply
> path_hprop change the goal.
>
> For people developing proofs:
> Improve Coq's error messages so that the error that you get when you leave
> out the apply path_hprop is sufficiently informative and not confusing.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/543/files#r18308819>.
>