Agreed. Done.
I'll come back about the canonical structures.
There is still a good example in hSet, I'll have some ideas for more, but
that should be another pull request.


On Mon, Sep 2, 2013 at 10:57 PM, Jason Gross <notifications@github.com>wrote:

> In theories/HProp.v:
>
> > -Lemma sigma_prop_eq {A} {P : A -> hProp}: forall u v : sigT P, u.1 = v.1 -> u=v.
> > -Proof.
> > -intros ? ? H.
> > -apply path_sigma with H. apply allpath_hprop.
> > -Defined.
> > +(** Every hProp is a subclass of IsHProp *)
> > +Record hProp := hp { hproptype : Type ; isp : IsHProp hproptype}.
> > +(** This one would allow us to turn the record type of contractible types into an [hProp].
> > +<<
> > +Canonical Structure default_HProp:= fun T P => (@hp T P).
> > +>>
> > +*)
> > +Existing Instance isp.
> > +(** Avoid hproptype, isp automatically eating a type *)
> > +Arguments hproptype :clear implicits.
> > +Arguments isp :clear implicits.
>
> Oops, I forgot to mention before, are these still needed? I think default
> implicit arguments are different for Class vs Record. If you keep this
> and the comment, hproptype, isp -> [hproptype], [isp] in the comment.
> Also, the Coercion can be done by replacing hproptype : Type with hproptype
> :> Type, now that it's a Record rather than a Class. (It's somewhat
> confusing that :> means Existing Instance for Class, but Coercion for
> Record.)
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6115018>
> .
>