Exercises 3.6 and 3.7

Question: why didn't I have to mention the use of Funext ?
It doesn't seem necessary to me unless there is alse a `_solution_2`.

On Fri, Sep 19, 2014 at 3:40 PM, Andrej Bauer <notifications@github.com>
wrote:

> In contrib/HoTTBookExercises.v:
>
> > @@ -386,12 +386,25 @@ Definition Book_3_5_solution_1 := @HoTT.HProp.equiv_hprop_inhabited_contr.
> >  (* ================================================== ex:lem-mereprop *)
> >  (** Exercise 3.6 *)
> >
> > -
> > +Lemma Book_3_6_solution_1 (A : Type) : IsHProp A -> IsHProp (A + ~A).
>
> Are we going to write _solution_1 all the time?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/519/files#r17813463>.
>