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.