implicit arguments in quotient.v, close #447

I think it should be outside.


On Mon, Sep 1, 2014 at 4:31 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/quotient.v:
>
> > @@ -67,16 +74,15 @@ Section Equiv.
> >
> >  Context `{Univalence}.
> >
> > -Context {A : Type} {R : relation A} {sR:setrel R}
> > +Context {A : Type} (R : relation A) {sR: forall x y, IsHProp (R x y)}
>
> setrel isn't defined here, since it's local to the module Quotient, I
> believe. This does raise the question, though, of why setrel is defined
> only within the module Quotient.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/450/files#r16956491>.
>