trunc_leq transparent & not an instance, no no-ops in trunc_contr

Also illustrates the fragility of universe annotations: changing the configuration of `IsTrunc` instances caused `ishprop_ooextendable` to take one fewer universe parameter.  Interestingly, results in a noticeable speedup, perhaps from smaller `IsTrunc` instances or fewer universes.
Ok, fixed.

On Mon, Nov 24, 2014 at 12:07 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/Basics/Trunc.v:
>
> > @@ -41,7 +41,8 @@ Proof.
> >    - apply IH, H.
> >  Qed.
> >
> > -Global Instance trunc_leq {m n} (Hmn : m <= n) `{IsTrunc m A} : IsTrunc n A | 1000.
> > +(** This could be an [Instance] (with very high priority, so it doesn't get applied trivially).  However, we haven't given typeclass search any hints allowing it to solve goals like [m <= n], so it wouldn't ever actually be used.  *)
>
>  it wouldn't ever actually be used
>
> This isn't true. Typeclass resolution will generally try reflexivity, so
> it'll only be used trivially, I think.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/623/files#r20817889>.
>