Beginning the overhaul. Sample of first 250 lines.

This is merely a sampler. Some remarks:

* The new file compiles.

* According to Benedikt's suggestion, I have begun structruring proofs with bullets, so that tactics are only applied to the subgoals they were meant to. A *very* quick introduction is available in [1].

[1] http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html
You're right, that's probably a bit too much; the original point was to
emphasize the location of the := sign.

I do, however, believe in redundant parentheses around the function
argument, which I have skipped in this particular case; e.g.

> fun (t : unit) => x

as it seems to improve readability in the case of multiple nested lambdas.

On 23 November 2014 15:03, Daniel R. Grayson <notifications@github.com>
wrote:

> In UniMath/Foundations/Generalities/uu0.v:
>
> >
> >  (** *** Functions from [ unit ] corresponding to terms *)
> >
> > -Definition termfun { X : UU } ( x : X ) : unit -> X := fun t : unit => x .
> > -
> > +Definition termfun {X : UU} (x : X) : unit -> X := (fun t : unit => x).
>
> Why do you choose to put redundant parentheses in around the function? I
> think it just adds visual clutter.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/UniMath/UniMath/pull/51/files#r20765027>.
>