I suggest we first accept this request and then pull Jason's.


On Tue, Sep 3, 2013 at 11:58 PM, Andrej Bauer <notifications@github.com>wrote:

> In theories/types/ObjectClassifier.v:
>
> > @@ -3,7 +3,9 @@ This equivalence is close to the existence of an object classifier.
> >  *)
> >
> >  Require Import HoTT Universe.
> > -Set Universe Polymorphism.
> > +Notation pr1:=(@projT1 _ _).
>
> Hasn't @JasonGross <https://github.com/JasonGross> just proposed that we
> get rid of pr1 and pr2? Which will it be?
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6139688>
> .
>