Further overhauling of (now) uu0a. Notice that the notation f ~ g
was introduced for homotopies, and consequently removed from the
K-Theory files due to conflict.
Merge remote-tracking branch 'upstream/master' into overhaul

Conflicts:
	UniMath/Foundations/Generalities/uu0a.v
Further beautification of uu0a. Reached homotopy fibers.
Further overhaul and beautification. Reached start of weak
equivalences.
Further overhauling.

There is only one substantial change: to deal with weak
equivalences, we introduce a function which, for each weak
equivalence and point in the codomain, gives the hfiber that is
the centre of contraction, of type

Definition weqccontrhfiber {X Y : UU} (w : weq X Y) (y : Y) : hfiber w y.

and a function which, for the same data, gives a proof of equality
of anything in the hfiber to this centre of contraction, of type

Definition weqccontrhfiber2 {X Y : UU} (w : weq X Y) (y : Y) :
  forall x : hfiber w y, x = weqccontrhfiber w y.
Adding notation "f comp g" for diagram-wise morphism composition.
Changed associativity of notation "f comp g" to left.
Some trouble with associativity levels -- pushed diagrammatic
composition up.
Removed notation f comp g, because of clashes with composition in
precategories. Issue to be discussed.
Merge pull request #64 from lambdabetaheta/overhaul

Further overhaul -- reached a little into weak equivalences