Some cosmetic changes mostly to hnat

More changes/additions to hnat to follow soon. 
I am not sure how it happened. They both should go to uu0b. It somehow happened when I was resolving the conflicts. Could you please put them back? I am not sure where to find them.





> On Dec 15, 2014, at 8:37 AM, Benedikt Ahrens <notifications@github.com> wrote:
> 
> In UniMath/Foundations/Generalities/uu0c.v <https://github.com/UniMath/UniMath/pull/65#discussion-diff-21823484>:
> 
> > -
> > -Lemma isweqonpathsincl { X Y : UU } (f:X -> Y) (is: isincl  f)(x x':X): isweq (@maponpaths _ _ f x x').
> > -Proof. intros. apply (isofhlevelfonpaths O  f x x' is). Defined.
> > -
> > -Definition weqonpathsincl  { X Y : UU } (f:X -> Y) (is: isincl  f)(x x':X) := weqpair _ ( isweqonpathsincl f is x x' ) .
> > -
> > -Definition invmaponpathsincl { X Y : UU } (f:X -> Y) (is: isincl  f)(x x':X): paths (f x) (f x') -> paths x x':= invmap  ( weqonpathsincl  f is x x') .
> > -
> > -
> > -Lemma isinclweqonpaths { X Y : UU } (f:X -> Y): (forall x x':X, isweq (@maponpaths _ _ f x x')) -> isincl  f.
> > -Proof. intros X Y f X0.  apply (isofhlevelfsn O  f X0). Defined.
> > -
> > -
> > -Definition isinclpr1 { X : UU } (P:X -> UU)(is: forall x:X, isaprop (P x)): isincl  (@pr1 X P):= isofhlevelfpr1 (S O) P is.
> > -
> > -Lemma total2_paths_isaprop (A : UU) (B : A -> UU) (is : forall a, isaprop (B a))
> This lemma (total2_paths_isaprop) was removed from uu0c, but not added anywhere else. Same for total2_paths_isaprop_equiv just below. However, some other stuff depends on those lemmas.
> 
> —
> Reply to this email directly or view it on GitHub <https://github.com/UniMath/UniMath/pull/65/files#r21823484>.
>