Thanks for the suggestions. They are fixed in the new commit.


On Mon, Sep 2, 2013 at 8:01 PM, Jason Gross <notifications@github.com>wrote:

> In theories/hit/quotient.v:
>
> > @@ -198,13 +198,13 @@ intros [f H].
> >  apply (quotient_rect_nondep _ H).
> >  Defined.
> >
> > +Require Import Misc.
> >  Theorem quotient_ump {funext_axiom:Funext} (B:hSet): (quotient _ -> B) <~>
>
> Tangent: {funext_axiom:Funext} can be removed here, and apply
> funext_axiom. below can be replaced by apply funext. (possibly also apply
> path_forall, though I haven't checked that one). I was confused when I
> saw funext_axiom being called an axiom. However, this is unrelated to
> this pull request, and I'll submit a separate pull request if you don't
> want to bother to fix that here.
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6114035>
> .
>