Thanks for the suggestions. I have now applied them in a new commit.

If it does not make sense, let me think a bit more, I need to run now.


On Fri, Aug 30, 2013 at 11:17 PM, Jason Gross <notifications@github.com>wrote:

> In theories/HProp.v:
>
> > -Global Existing Instance isp.
> > -
> > -Definition issig_hProp
> > -: { propT : Type & IsHProp propT } <~> hProp.
> > -Proof.
> > -  issig BuildhProp propT isp.
> > +(** We use both the Sigma type of propositions and the record type of propositions.
> > +The latter allows us to automatically find a proof that a type is a proposition.
> > +
> > +Setting things up in this way allows us to define coercions from one type to the other.
> > +So, a theory stated about one type can be apply to the other. It's not magic, but it is convenient.
> > +
> > +We should explore this some more and then apply this to more record types.
> > +*)
> > +
> > +Class total2 {T} (P: T -> Type) := tpair2 { tp1 :> T ; tp2 :> P tp1 }.
>
> What does having total2 add? In particular, why do we want it to be a
> class (i.e., why can't we just use sigT), and why do we want it to be
> inconvertible with sigT (i.e., why isn't this Class total2 {T} {P : T ->
> Type} := tpair2 : sigT P)?
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6096467>
> .
>