Why will exercises need more explanation and code, rather than being just
formalizations of the solutions in exercise_solutions.tex?

FWIW, there are some exercises that I think will definitely correspond to
theorems in the main library.  Perhaps in the second edition those
exercises will become theorems, but for now they are exercises.
On Dec 30, 2013 4:02 AM, "Edward Z. Yang" <notifications@github.com> wrote:

> In contrib/HoTTBook.v:
>
> >  (* ================================================== ex:pr-to-rec *)
> >  (** Exercise 1.2 *)
> >
> > -
> > +(** Recursor as equivalence. *)
> > +Definition Book_1_2_prod_lib := @equiv_uncurry.
> > +Section Book_1_2_prod.
> > +  Variable A B : Type.
> > +
> > +  (** Recursor with projection functions instead of pattern-matching. *)
>
> Here's my opinion: the exercises should not be in HoTTBook.v; instead,
> they should be separated into their own file. Exercises in general will
> need a bit more explanation and contain more code, and generally one isn't
> going to be flipping through the exercises looking for a theorem they need
> in the main library.
>
> (The fuss, by the way, is because the exercise asks for it, and isn't
> actually an important distinction.)
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/302/files#r8583759>
> .
>