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.
Changes to hnat, mostly replacing names with notations
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.
Some more cosmetic changes to hnat
A modification, with an eye on teaching, of fromempty
Removed notation f comp g, because of clashes with composition in
precategories. Issue to be discussed.
Resoved a conflict related to moving some material from uu0c to uu0b
Completeing a pull request
reinserted 2 lemmas about paths in total2
Merge pull request #16 from benediktahrens/vv-master

reinserted 2 lemmas about paths in total2
Merge pull request #64 from lambdabetaheta/overhaul

Further overhaul -- reached a little into weak equivalences
Further overhauling. Reached the Grad Theorem.
Removed homotopy notation from the statement of isweqhomot, as it breaks algebra1a.
Merge pull request #65 from vladimirias/master

Some cosmetic changes mostly to hnat